Theorem opeq1 4080

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

Assertion

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

Proof of Theorem opeq1

Step	Hyp	Ref	Expression
1		eleq1 2503	. . . 4 |- ( A = B -> ( A e. _V <-> B e. _V ) )
2	1	anbi1d 704	. . 3 |- ( A = B -> ( ( A e. _V /\ C e. _V ) <-> ( B e. _V /\ C e. _V ) ) )
3		sneq 3908	. . . 4 |- ( A = B -> { A } = { B } )
4		preq1 3975	. . . 4 |- ( A = B -> { A , C } = { B , C } )
5	3, 4	preq12d 3983	. . 3 |- ( A = B -> { { A } , { A , C } } = { { B } , { B , C } } )
6	2, 5	ifbieq1d 3833	. 2 |- ( A = B -> if ( ( A e. _V /\ C e. _V ) , { { A } , { A , C } } , (/) ) = if ( ( B e. _V /\ C e. _V ) , { { B } , { B , C } } , (/) ) )
7		dfopif 4077	. 2 |- <. A , C >. = if ( ( A e. _V /\ C e. _V ) , { { A } , { A , C } } , (/) )
8		dfopif 4077	. 2 |- <. B , C >. = if ( ( B e. _V /\ C e. _V ) , { { B } , { B , C } } , (/) )
9	6, 7, 8	3eqtr4g 2500	1 |- ( A = B -> <. A , C >. = <. B , C >. )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1369   e. wcel 1756   _Vcvv 2993   (/)c0 3658   ifcif 3812   {csn 3898   {cpr 3900   <.cop 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905

This theorem is referenced by:  opeq12  4082  opeq1i  4083  opeq1d  4086  oteq1  4089  breq1  4316  cbvopab1  4383  cbvopab1s  4385  opthg  4588  eqvinop  4596  opelopabsb  4620  opelxp  4890  elvvv  4919  opabid2  4990  opeliunxp2  4999  elsnres  5167  elimasng  5216  dmsnopg  5331  cnvsng  5346  funopg  5471  f1osng  5700  f1oprswap  5701  dmfco  5786  fvelrn  5860  fsng  5903  fprg  5912  fvsng  5933  funfvima3  5975  oveq1  6119  oprabid  6136  dfoprab2  6154  cbvoprab1  6179  elxp4  6543  elxp5  6544  opabex3d  6576  opabex3  6577  op1stg  6610  op2ndg  6611  dfoprab4f  6653  frxp  6703  tfrlem11  6868  omeu  7045  oeeui  7062  elixpsn  7323  fundmen  7404  xpsnen  7416  xpassen  7426  xpf1o  7494  unxpdomlem1  7538  dfac5lem1  8314  dfac5lem4  8317  axdc4lem  8645  nqereu  9119  mulcanenq  9150  archnq  9170  prlem934  9223  supsrlem  9299  supsr  9300  swrdccatin1  12395  swrdccat3blem  12407  fsum2dlem  13258  vdwlem10  14072  imasaddfnlem  14487  catideu  14634  iscatd2  14640  catlid  14642  catpropd  14669  symg2bas  15924  efgmval  16230  efgi  16237  vrgpval  16285  gsumcom2  16489  txkgen  19247  cnmpt21  19266  xkoinjcn  19282  txcon  19284  pt1hmeo  19401  cnextfvval  19659  divstgplem  19713  dvbsss  21399  axlowdim2  23228  axlowdim  23229  axcontlem10  23241  axcontlem12  23243  drngoi  23916  isdivrngo  23940  isnvlem  24010  br8d  25964  cnvoprab  26045  prsrn  26367  eulerpartlemgvv  26781  fprod2dlem  27513  br8  27588  br6  27589  br4  27590  eldm3  27594  dfdm5  27609  elfuns  27968  brimg  27990  brapply  27991  brrestrict  28002  dfrdg4  28003  cgrdegen  28057  brofs  28058  cgrextend  28061  brifs  28096  ifscgr  28097  brcgr3  28099  brcolinear2  28111  colineardim1  28114  brfs  28132  idinside  28137  btwnconn1lem7  28146  btwnconn1lem11  28150  btwnconn1lem12  28151  brsegle  28161  outsideofeu  28184  fvray  28194  linedegen  28196  fvline  28197  dropab1  29729  el2xptp  30152  fvelrnfvelrnressn  30177  0eusgraiff0rgra  30578  relopabVD  31733  bj-inftyexpiinv  32627  bj-inftyexpidisj  32629  dicelval3  34921  dihjatcclem4  35162