Theorem opeq2 3820

Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)

Assertion

Ref	Expression
opeq2	|- ( A = B -> <. C , A >. = <. C , B >. )

Proof of Theorem opeq2

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2268	. . . . . 6 |- ( A = B -> ( A e. _V <-> B e. _V ) )
2	1	anbi2d 464	. . . . 5 |- ( A = B -> ( ( C e. _V /\ A e. _V ) <-> ( C e. _V /\ B e. _V ) ) )
3		eqidd 2206	. . . . . . 7 |- ( A = B -> { C } = { C } )
4		preq2 3711	. . . . . . 7 |- ( A = B -> { C , A } = { C , B } )
5	3, 4	preq12d 3718	. . . . . 6 |- ( A = B -> { { C } , { C , A } } = { { C } , { C , B } } )
6	5	eleq2d 2275	. . . . 5 |- ( A = B -> ( x e. { { C } , { C , A } } <-> x e. { { C } , { C , B } } ) )
7	2, 6	anbi12d 473	. . . 4 |- ( A = B -> ( ( ( C e. _V /\ A e. _V ) /\ x e. { { C } , { C , A } } ) <-> ( ( C e. _V /\ B e. _V ) /\ x e. { { C } , { C , B } } ) ) )
8		df-3an 983	. . . 4 |- ( ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) <-> ( ( C e. _V /\ A e. _V ) /\ x e. { { C } , { C , A } } ) )
9		df-3an 983	. . . 4 |- ( ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) <-> ( ( C e. _V /\ B e. _V ) /\ x e. { { C } , { C , B } } ) )
10	7, 8, 9	3bitr4g 223	. . 3 |- ( A = B -> ( ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) <-> ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) ) )
11	10	abbidv 2323	. 2 |- ( A = B -> { x | ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) } = { x | ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) } )
12		df-op 3642	. 2 |- <. C , A >. = { x | ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) }
13		df-op 3642	. 2 |- <. C , B >. = { x | ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) }
14	11, 12, 13	3eqtr4g 2263	1 |- ( A = B -> <. C , A >. = <. C , B >. )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 981   = wceq 1373   e. wcel 2176   {cab 2191   _Vcvv 2772   {csn 3633   {cpr 3634   <.cop 3636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642

This theorem is referenced by:  opeq12  3821  opeq2i  3823  opeq2d  3826  oteq2  3829  oteq3  3830  breq2  4048  cbvopab2  4118  cbvopab2v  4121  opthg  4282  eqvinop  4287  opelopabsb  4306  opelxp  4705  opabid2  4809  elrn2g  4868  opeldm  4881  opeldmg  4883  elrn2  4920  opelresg  4966  iss  5005  elimasng  5050  issref  5065  dmsnopg  5154  cnvsng  5168  elxp4  5170  elxp5  5171  dffun5r  5283  funopg  5305  f1osng  5563  tz6.12f  5605  fsn  5752  fsng  5753  fvsng  5780  oveq2  5952  cbvoprab2  6018  ovg  6085  opabex3d  6206  opabex3  6207  op1stg  6236  op2ndg  6237  oprssdmm  6257  op1steq  6265  dfoprab4f  6279  tfrlemibxssdm  6413  tfr1onlembxssdm  6429  tfrcllembxssdm  6442  elixpsn  6822  ixpsnf1o  6823  mapsnen  6903  xpsnen  6916  xpassen  6925  xpf1o  6941  djulclr  7151  djurclr  7152  djulcl  7153  djurcl  7154  djulclb  7157  inl11  7167  djuss  7172  1stinl  7176  2ndinl  7177  1stinr  7178  2ndinr  7179  elreal  7941  ax1rid  7990  fseq1p1m1  10216  imasaddfnlemg  13146  cnmpt21  14763  djucllem  15740