Theorem eqvinop

Description: A variable introduction law for ordered pairs. Analogue of Lemma 15 of Monk2 p. 109. (Contributed by NM, 28-May-1995)

	Ref	Expression
Hypotheses	eqvinop.1	|- B e. _V
	eqvinop.2	|- C e. _V
Assertion	eqvinop	|- ( A = <. B , C >. <-> E. x E. y ( A = <. x , y >. /\ <. x , y >. = <. B , C >. ) )

Proof

Step	Hyp	Ref	Expression
1		eqvinop.1	|- B e. _V
2		eqvinop.2	|- C e. _V
3	1 2	opth2	|- ( <. x , y >. = <. B , C >. <-> ( x = B /\ y = C ) )
4	3	anbi2i	|- ( ( A = <. x , y >. /\ <. x , y >. = <. B , C >. ) <-> ( A = <. x , y >. /\ ( x = B /\ y = C ) ) )
5		ancom	|- ( ( A = <. x , y >. /\ ( x = B /\ y = C ) ) <-> ( ( x = B /\ y = C ) /\ A = <. x , y >. ) )
6		anass	|- ( ( ( x = B /\ y = C ) /\ A = <. x , y >. ) <-> ( x = B /\ ( y = C /\ A = <. x , y >. ) ) )
7	4 5 6	3bitri	|- ( ( A = <. x , y >. /\ <. x , y >. = <. B , C >. ) <-> ( x = B /\ ( y = C /\ A = <. x , y >. ) ) )
8	7	exbii	|- ( E. y ( A = <. x , y >. /\ <. x , y >. = <. B , C >. ) <-> E. y ( x = B /\ ( y = C /\ A = <. x , y >. ) ) )
9		19.42v	|- ( E. y ( x = B /\ ( y = C /\ A = <. x , y >. ) ) <-> ( x = B /\ E. y ( y = C /\ A = <. x , y >. ) ) )
10		opeq2	|- ( y = C -> <. x , y >. = <. x , C >. )
11	10	eqeq2d	|- ( y = C -> ( A = <. x , y >. <-> A = <. x , C >. ) )
12	2 11	ceqsexv	|- ( E. y ( y = C /\ A = <. x , y >. ) <-> A = <. x , C >. )
13	12	anbi2i	|- ( ( x = B /\ E. y ( y = C /\ A = <. x , y >. ) ) <-> ( x = B /\ A = <. x , C >. ) )
14	8 9 13	3bitri	|- ( E. y ( A = <. x , y >. /\ <. x , y >. = <. B , C >. ) <-> ( x = B /\ A = <. x , C >. ) )
15	14	exbii	|- ( E. x E. y ( A = <. x , y >. /\ <. x , y >. = <. B , C >. ) <-> E. x ( x = B /\ A = <. x , C >. ) )
16		opeq1	|- ( x = B -> <. x , C >. = <. B , C >. )
17	16	eqeq2d	|- ( x = B -> ( A = <. x , C >. <-> A = <. B , C >. ) )
18	1 17	ceqsexv	|- ( E. x ( x = B /\ A = <. x , C >. ) <-> A = <. B , C >. )
19	15 18	bitr2i	|- ( A = <. B , C >. <-> E. x E. y ( A = <. x , y >. /\ <. x , y >. = <. B , C >. ) )