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

Metamath Proof Explorer

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 >. ) )