This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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