Metamath Proof Explorer

Theorem cllem0

Description: The class of all sets with property ph ( z ) is closed under the binary operation on sets defined in R ( x , y ) . (Contributed by RP, 3-Jan-2020)

Ref Expression
Hypotheses cllem0.v ⊢V=z|φ
cllem0.rex ⊢R∈U
cllem0.r ⊢z=R→φ↔ψ
cllem0.x ⊢z=x→φ↔χ
cllem0.y ⊢z=y→φ↔θ
cllem0.closed ⊢χ∧θ→ψ
Assertion cllem0 ⊢∀x∈V∀y∈VR∈V

Proof

Step Hyp Ref Expression
1 cllem0.v ⊢V=z|φ
2 cllem0.rex ⊢R∈U
3 cllem0.r ⊢z=R→φ↔ψ
4 cllem0.x ⊢z=x→φ↔χ
5 cllem0.y ⊢z=y→φ↔θ
6 cllem0.closed ⊢χ∧θ→ψ
7 2 elexi ⊢R∈V
8 7 3 1 elab2 ⊢R∈V↔ψ
9 8 ralbii ⊢∀y∈VR∈V↔∀y∈Vψ
10 9 ralbii ⊢∀x∈V∀y∈VR∈V↔∀x∈V∀y∈Vψ
11 df-ral ⊢∀y∈Vψ↔∀yy∈V→ψ
12 11 ralbii ⊢∀x∈V∀y∈Vψ↔∀x∈V∀yy∈V→ψ
13 df-ral ⊢∀x∈V∀yy∈V→ψ↔∀xx∈V→∀yy∈V→ψ
14 10 12 13 3bitri ⊢∀x∈V∀y∈VR∈V↔∀xx∈V→∀yy∈V→ψ
15 vex ⊢x∈V
16 15 4 1 elab2 ⊢x∈V↔χ
17 vex ⊢y∈V
18 17 5 1 elab2 ⊢y∈V↔θ
19 16 18 6 syl2anb ⊢x∈V∧y∈V→ψ
20 19 ex ⊢x∈V→y∈V→ψ
21 20 alrimiv ⊢x∈V→∀yy∈V→ψ
22 14 21 mpgbir ⊢∀x∈V∀y∈VR∈V