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