Theorem elovmpod

Description: Utility lemma for two-parameter classes. (Contributed by Stefan O'Rear, 21-Jan-2015) Variant of elovmpo in deduction form. (Revised by AV, 20-Apr-2025)

	Ref	Expression
Hypotheses	elovmpod.o	|- O = ( a e. A , b e. B |-> C )
	elovmpod.x	|- ( ph -> X e. A )
	elovmpod.y	|- ( ph -> Y e. B )
	elovmpod.d	|- ( ph -> D e. V )
	elovmpod.c	|- ( ( a = X /\ b = Y ) -> C = D )
Assertion	elovmpod	|- ( ph -> ( E e. ( X O Y ) <-> E e. D ) )

Proof

Step	Hyp	Ref	Expression
1		elovmpod.o	|- O = ( a e. A , b e. B |-> C )
2		elovmpod.x	|- ( ph -> X e. A )
3		elovmpod.y	|- ( ph -> Y e. B )
4		elovmpod.d	|- ( ph -> D e. V )
5		elovmpod.c	|- ( ( a = X /\ b = Y ) -> C = D )
6	1	a1i	|- ( ph -> O = ( a e. A , b e. B |-> C ) )
7	5	adantl	|- ( ( ph /\ ( a = X /\ b = Y ) ) -> C = D )
8	6 7 2 3 4	ovmpod	|- ( ph -> ( X O Y ) = D )
9	8	eleq2d	|- ( ph -> ( E e. ( X O Y ) <-> E e. D ) )