Theorem opeq2 3779

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 2240	. . . . . 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 2178	. . . . . . 7 |- ( A = B -> { C } = { C } )
4		preq2 3670	. . . . . . 7 |- ( A = B -> { C , A } = { C , B } )
5	3, 4	preq12d 3677	. . . . . 6 |- ( A = B -> { { C } , { C , A } } = { { C } , { C , B } } )
6	5	eleq2d 2247	. . . . 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 980	. . . 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 980	. . . 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 2295	. 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 3601	. 2 |- <. C , A >. = { x | ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) }
13		df-op 3601	. 2 |- <. C , B >. = { x | ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) }
14	11, 12, 13	3eqtr4g 2235	1 |- ( A = B -> <. C , A >. = <. C , B >. )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 978   = wceq 1353   e. wcel 2148   {cab 2163   _Vcvv 2737   {csn 3592   {cpr 3593   <.cop 3595

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601

This theorem is referenced by:  opeq12  3780  opeq2i  3782  opeq2d  3785  oteq2  3788  oteq3  3789  breq2  4007  cbvopab2  4077  cbvopab2v  4080  opthg  4238  eqvinop  4243  opelopabsb  4260  opelxp  4656  opabid2  4758  elrn2g  4817  opeldm  4830  opeldmg  4832  elrn2  4869  opelresg  4914  iss  4953  elimasng  4996  issref  5011  dmsnopg  5100  cnvsng  5114  elxp4  5116  elxp5  5117  dffun5r  5228  funopg  5250  f1osng  5502  tz6.12f  5544  fsn  5688  fsng  5689  fvsng  5712  oveq2  5882  cbvoprab2  5947  ovg  6012  opabex3d  6121  opabex3  6122  op1stg  6150  op2ndg  6151  oprssdmm  6171  op1steq  6179  dfoprab4f  6193  tfrlemibxssdm  6327  tfr1onlembxssdm  6343  tfrcllembxssdm  6356  elixpsn  6734  ixpsnf1o  6735  mapsnen  6810  xpsnen  6820  xpassen  6829  xpf1o  6843  djulclr  7047  djurclr  7048  djulcl  7049  djurcl  7050  djulclb  7053  inl11  7063  djuss  7068  1stinl  7072  2ndinl  7073  1stinr  7074  2ndinr  7075  elreal  7826  ax1rid  7875  fseq1p1m1  10091  imasaddfnlemg  12717  cnmpt21  13684  djucllem  14434