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 ∈ V R ∈ 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 ∈ V R ∈ V ↔ ∀ y ∈ V ψ
10 9 ralbii ⊢ ∀ x ∈ V ∀ y ∈ V R ∈ V ↔ ∀ x ∈ V ∀ y ∈ V ψ
11 df-ral ⊢ ∀ y ∈ V ψ ↔ ∀ y y ∈ V → ψ
12 11 ralbii ⊢ ∀ x ∈ V ∀ y ∈ V ψ ↔ ∀ x ∈ V ∀ y y ∈ V → ψ
13 df-ral ⊢ ∀ x ∈ V ∀ y y ∈ V → ψ ↔ ∀ x x ∈ V → ∀ y y ∈ V → ψ
14 10 12 13 3bitri ⊢ ∀ x ∈ V ∀ y ∈ V R ∈ V ↔ ∀ x x ∈ V → ∀ y y ∈ 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 → ∀ y y ∈ V → ψ
22 14 21 mpgbir ⊢ ∀ x ∈ V ∀ y ∈ V R ∈ V