Theorem opeq1 3944

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 2464	. . . 4 |- ( A = B -> ( A e. _V <-> B e. _V ) )
2	1	anbi1d 686	. . 3 |- ( A = B -> ( ( A e. _V /\ C e. _V ) <-> ( B e. _V /\ C e. _V ) ) )
3		sneq 3785	. . . 4 |- ( A = B -> { A } = { B } )
4		preq1 3843	. . . 4 |- ( A = B -> { A , C } = { B , C } )
5	3, 4	preq12d 3851	. . 3 |- ( A = B -> { { A } , { A , C } } = { { B } , { B , C } } )
6		eqidd 2405	. . 3 |- ( A = B -> (/) = (/) )
7	2, 5, 6	ifbieq12d 3721	. 2 |- ( A = B -> if ( ( A e. _V /\ C e. _V ) , { { A } , { A , C } } , (/) ) = if ( ( B e. _V /\ C e. _V ) , { { B } , { B , C } } , (/) ) )
8		dfopif 3941	. 2 |- <. A , C >. = if ( ( A e. _V /\ C e. _V ) , { { A } , { A , C } } , (/) )
9		dfopif 3941	. 2 |- <. B , C >. = if ( ( B e. _V /\ C e. _V ) , { { B } , { B , C } } , (/) )
10	7, 8, 9	3eqtr4g 2461	1 |- ( A = B -> <. A , C >. = <. B , C >. )

Syntax hints:   -> wi 4   /\ wa 359   = wceq 1649   e. wcel 1721   _Vcvv 2916   (/)c0 3588   ifcif 3699   {csn 3774   {cpr 3775   <.cop 3777

This theorem is referenced by:  opeq12  3946  opeq1i  3947  opeq1d  3950  oteq1  3953  breq1  4175  cbvopab1  4238  cbvopab1s  4240  opthg  4396  eqvinop  4401  opelopabsb  4425  opelxp  4867  elvvv  4896  opabid2  4963  opeliunxp2  4972  elsnres  5141  elimasng  5189  dmsnopg  5300  cnvsng  5314  elxp4  5316  elxp5  5317  funopg  5444  f1osng  5675  f1oprswap  5676  dmfco  5756  fvelrn  5825  fsng  5866  fprg  5874  fvsng  5886  funfvima3  5934  opabex3d  5948  opabex3  5949  oveq1  6047  oprabid  6064  dfoprab2  6080  cbvoprab1  6103  op1stg  6318  op2ndg  6319  dfoprab4f  6364  frxp  6415  tfrlem11  6608  omeu  6787  oeeui  6804  elixpsn  7060  fundmen  7139  xpsnen  7151  xpassen  7161  xpf1o  7228  unxpdomlem1  7272  dfac5lem1  7960  dfac5lem4  7963  axdc4lem  8291  nqereu  8762  mulcanenq  8793  archnq  8813  prlem934  8866  supsrlem  8942  supsr  8943  fsum2dlem  12509  vdwlem10  13313  imasaddfnlem  13708  catideu  13855  iscatd2  13861  catlid  13863  catpropd  13890  efgmval  15299  efgi  15306  vrgpval  15354  gsumcom2  15504  txkgen  17637  cnmpt21  17656  xkoinjcn  17672  txcon  17674  pt1hmeo  17791  cnextfvval  18049  divstgplem  18103  dvbsss  19742  drngoi  21948  isdivrngo  21972  isnvlem  22042  fprod2dlem  25257  br8  25327  br6  25328  br4  25329  eldm3  25333  dfdm5  25346  brimg  25690  brapply  25691  brrestrict  25702  dfrdg4  25703  axlowdim2  25803  axlowdim  25804  axcontlem10  25816  axcontlem12  25818  cgrdegen  25842  brofs  25843  cgrextend  25846  brifs  25881  ifscgr  25882  brcgr3  25884  brcolinear2  25896  colineardim1  25899  brfs  25917  idinside  25922  btwnconn1lem7  25931  btwnconn1lem11  25935  btwnconn1lem12  25936  brsegle  25946  outsideofeu  25969  fvray  25979  linedegen  25981  fvline  25982  dropab1  27517  el2xptp  27948  swrdccatin1  28016  relopabVD  28722  dicelval3  31663  dihjatcclem4  31904

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783