Theorem elovmpo

Description: Utility lemma for two-parameter classes.

EDITORIAL: can simplify isghm , islmhm . (Contributed by Stefan O'Rear, 21-Jan-2015)

	Ref	Expression
Hypotheses	elovmpo.d	|- D = ( a e. A , b e. B |-> C )
	elovmpo.c	|- C e. _V
	elovmpo.e	|- ( ( a = X /\ b = Y ) -> C = E )
Assertion	elovmpo	|- ( F e. ( X D Y ) <-> ( X e. A /\ Y e. B /\ F e. E ) )

Proof

Step	Hyp	Ref	Expression
1		elovmpo.d	|- D = ( a e. A , b e. B |-> C )
2		elovmpo.c	|- C e. _V
3		elovmpo.e	|- ( ( a = X /\ b = Y ) -> C = E )
4	1	elmpocl	|- ( F e. ( X D Y ) -> ( X e. A /\ Y e. B ) )
5	2	gen2	|- A. a A. b C e. _V
6	3	eleq1d	|- ( ( a = X /\ b = Y ) -> ( C e. _V <-> E e. _V ) )
7	6	spc2gv	|- ( ( X e. A /\ Y e. B ) -> ( A. a A. b C e. _V -> E e. _V ) )
8	5 7	mpi	|- ( ( X e. A /\ Y e. B ) -> E e. _V )
9	3 1	ovmpoga	|- ( ( X e. A /\ Y e. B /\ E e. _V ) -> ( X D Y ) = E )
10	8 9	mpd3an3	|- ( ( X e. A /\ Y e. B ) -> ( X D Y ) = E )
11	10	eleq2d	|- ( ( X e. A /\ Y e. B ) -> ( F e. ( X D Y ) <-> F e. E ) )
12	4 11	biadanii	|- ( F e. ( X D Y ) <-> ( ( X e. A /\ Y e. B ) /\ F e. E ) )
13		df-3an	|- ( ( X e. A /\ Y e. B /\ F e. E ) <-> ( ( X e. A /\ Y e. B ) /\ F e. E ) )
14	12 13	bitr4i	|- ( F e. ( X D Y ) <-> ( X e. A /\ Y e. B /\ F e. E ) )