Metamath Proof Explorer

Theorem relopabi

Description: A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013) Remove dependency on ax-sep , ax-nul , ax-pr . (Revised by KP, 25-Oct-2021) Avoid ax-11 and ax-12 . (Revised by SN, 26-Oct-2026)

Ref Expression
Hypothesis relopabi.1 
|- A = { <. x , y >. | ph }
Assertion relopabi 
|- Rel A

Proof

Step Hyp Ref Expression
1 relopabi.1 
 |-  A = { <. x , y >. | ph }
2 vex 
 |-  x e. _V
3 vex 
 |-  y e. _V
4 2 3 pm3.2i 
 |-  ( x e. _V /\ y e. _V )
5 4 a1i 
 |-  ( ph -> ( x e. _V /\ y e. _V ) )
6 5 ssopab2i 
 |-  { <. x , y >. | ph } C_ { <. x , y >. | ( x e. _V /\ y e. _V ) }
7 ax6evr 
 |-  E. u x = u
8 ax6evr 
 |-  E. v y = v
9 opeq12 
 |-  ( ( x = u /\ y = v ) -> <. x , y >. = <. u , v >. )
10 9 eqeq2d 
 |-  ( ( x = u /\ y = v ) -> ( z = <. x , y >. <-> z = <. u , v >. ) )
11 10 biimpd 
 |-  ( ( x = u /\ y = v ) -> ( z = <. x , y >. -> z = <. u , v >. ) )
12 11 ex 
 |-  ( x = u -> ( y = v -> ( z = <. x , y >. -> z = <. u , v >. ) ) )
13 12 eximdv 
 |-  ( x = u -> ( E. v y = v -> E. v ( z = <. x , y >. -> z = <. u , v >. ) ) )
14 8 13 mpi 
 |-  ( x = u -> E. v ( z = <. x , y >. -> z = <. u , v >. ) )
15 19.37imv 
 |-  ( E. v ( z = <. x , y >. -> z = <. u , v >. ) -> ( z = <. x , y >. -> E. v z = <. u , v >. ) )
16 14 15 syl 
 |-  ( x = u -> ( z = <. x , y >. -> E. v z = <. u , v >. ) )
17 7 16 eximii 
 |-  E. u ( z = <. x , y >. -> E. v z = <. u , v >. )
18 17 19.37iv 
 |-  ( z = <. x , y >. -> E. u E. v z = <. u , v >. )
19 18 exlimivv 
 |-  ( E. x E. y z = <. x , y >. -> E. u E. v z = <. u , v >. )
20 19 ss2abi 
 |-  { z | E. x E. y z = <. x , y >. } C_ { z | E. u E. v z = <. u , v >. }
21 4 biantru 
 |-  ( z = <. x , y >. <-> ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) )
22 21 2exbii 
 |-  ( E. x E. y z = <. x , y >. <-> E. x E. y ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) )
23 22 abbii 
 |-  { z | E. x E. y z = <. x , y >. } = { z | E. x E. y ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) }
24 vex 
 |-  u e. _V
25 vex 
 |-  v e. _V
26 24 25 pm3.2i 
 |-  ( u e. _V /\ v e. _V )
27 26 biantru 
 |-  ( z = <. u , v >. <-> ( z = <. u , v >. /\ ( u e. _V /\ v e. _V ) ) )
28 27 2exbii 
 |-  ( E. u E. v z = <. u , v >. <-> E. u E. v ( z = <. u , v >. /\ ( u e. _V /\ v e. _V ) ) )
29 28 abbii 
 |-  { z | E. u E. v z = <. u , v >. } = { z | E. u E. v ( z = <. u , v >. /\ ( u e. _V /\ v e. _V ) ) }
30 20 23 29 3sstr3i 
 |-  { z | E. x E. y ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) } C_ { z | E. u E. v ( z = <. u , v >. /\ ( u e. _V /\ v e. _V ) ) }
31 df-opab 
 |-  { <. x , y >. | ( x e. _V /\ y e. _V ) } = { z | E. x E. y ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) }
32 df-opab 
 |-  { <. u , v >. | ( u e. _V /\ v e. _V ) } = { z | E. u E. v ( z = <. u , v >. /\ ( u e. _V /\ v e. _V ) ) }
33 30 31 32 3sstr4i 
 |-  { <. x , y >. | ( x e. _V /\ y e. _V ) } C_ { <. u , v >. | ( u e. _V /\ v e. _V ) }
34 df-xp 
 |-  ( _V X. _V ) = { <. u , v >. | ( u e. _V /\ v e. _V ) }
35 33 34 sseqtrri 
 |-  { <. x , y >. | ( x e. _V /\ y e. _V ) } C_ ( _V X. _V )
36 6 35 sstri 
 |-  { <. x , y >. | ph } C_ ( _V X. _V )
37 1 36 eqsstri 
 |-  A C_ ( _V X. _V )
38 df-rel 
 |-  ( Rel A <-> A C_ ( _V X. _V ) )
39 37 38 mpbir 
 |-  Rel A