rintro a ha b hb rfl
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ ∀ (x_1 : V), x_1 ∈ x → ∀ (x_2 : V), x_2 ∈ y → z = opair x_1 x_2 → z ⊆ power (x ∪ y)
V : Type u_1
inst✝ : Zermelo V
x y a : V
ha : a ∈ x
b : V
hb : b ∈ y
⊢ opair a b ⊆ power (x ∪ y)