Theorem copsex2dv

Description: Implicit substitution deduction for ordered pairs. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	copsex2dv.a	|- ( ph -> A e. U )
	copsex2dv.b	|- ( ph -> B e. V )
	copsex2dv.1	|- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )
Assertion	copsex2dv	|- ( ph -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ch ) )

Proof

Step	Hyp	Ref	Expression
1		copsex2dv.a	|- ( ph -> A e. U )
2		copsex2dv.b	|- ( ph -> B e. V )
3		copsex2dv.1	|- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )
4	3	ex	|- ( ph -> ( ( x = A /\ y = B ) -> ( ps <-> ch ) ) )
5	4	alrimivv	|- ( ph -> A. x A. y ( ( x = A /\ y = B ) -> ( ps <-> ch ) ) )
6		copsex2t	|- ( ( A. x A. y ( ( x = A /\ y = B ) -> ( ps <-> ch ) ) /\ ( A e. U /\ B e. V ) ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ch ) )
7	5 1 2 6	syl12anc	|- ( ph -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ch ) )