Theorem relopabiALT

Description: Alternate proof of relopabi (shorter but uses more axioms). (Contributed by Mario Carneiro, 21-Dec-2013) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		relopabi.1	|- A = { <. x , y >. | ph }
2		df-opab	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
3	1 2	eqtri	|- A = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
4		vex	|- x e. _V
5		vex	|- y e. _V
6	4 5	opelvv	|- <. x , y >. e. ( _V X. _V )
7		eleq1	|- ( z = <. x , y >. -> ( z e. ( _V X. _V ) <-> <. x , y >. e. ( _V X. _V ) ) )
8	6 7	mpbiri	|- ( z = <. x , y >. -> z e. ( _V X. _V ) )
9	8	adantr	|- ( ( z = <. x , y >. /\ ph ) -> z e. ( _V X. _V ) )
10	9	exlimivv	|- ( E. x E. y ( z = <. x , y >. /\ ph ) -> z e. ( _V X. _V ) )
11	10	abssi	|- { z | E. x E. y ( z = <. x , y >. /\ ph ) } C_ ( _V X. _V )
12	3 11	eqsstri	|- A C_ ( _V X. _V )
13		df-rel	|- ( Rel A <-> A C_ ( _V X. _V ) )
14	12 13	mpbir	|- Rel A