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