Metamath Proof Explorer


Theorem relopabiv

Description: A class of ordered pairs is a relation. For a version without a disjoint variable condition, but a longer proof using ax-11 and ax-12 , see relopabi . (Contributed by BJ, 22-Jul-2023)

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

Proof

Step Hyp Ref Expression
1 relopabiv.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 df-xp
 |-  ( _V X. _V ) = { <. x , y >. | ( x e. _V /\ y e. _V ) }
8 6 1 7 3sstr4i
 |-  A C_ ( _V X. _V )
9 df-rel
 |-  ( Rel A <-> A C_ ( _V X. _V ) )
10 8 9 mpbir
 |-  Rel A