Theorem opeq1 4136

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 2518	. . . 4 |- ( A = B -> ( A e. _V <-> B e. _V ) )
2	1	anbi1d 716	. . 3 |- ( A = B -> ( ( A e. _V /\ C e. _V ) <-> ( B e. _V /\ C e. _V ) ) )
3		sneq 3946	. . . 4 |- ( A = B -> { A } = { B } )
4		preq1 4020	. . . 4 |- ( A = B -> { A , C } = { B , C } )
5	3, 4	preq12d 4028	. . 3 |- ( A = B -> { { A } , { A , C } } = { { B } , { B , C } } )
6	2, 5	ifbieq1d 3872	. 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 4133	. 2 |- <. A , C >. = if ( ( A e. _V /\ C e. _V ) , { { A } , { A , C } } , (/) )
8		dfopif 4133	. 2 |- <. B , C >. = if ( ( B e. _V /\ C e. _V ) , { { B } , { B , C } } , (/) )
9	6, 7, 8	3eqtr4g 2511	1 |- ( A = B -> <. A , C >. = <. B , C >. )

Syntax hints:   -> wi 4   /\ wa 375   = wceq 1448   e. wcel 1891   _Vcvv 3013   (/)c0 3699   ifcif 3849   {csn 3936   {cpr 3938   <.cop 3942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-rab 2746  df-v 3015  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943

This theorem is referenced by:  opeq12  4138  opeq1i  4139  opeq1d  4142  oteq1  4145  breq1  4377  cbvopab1  4445  cbvopab1s  4447  opthg  4650  eqvinop  4659  opelopabsb  4684  opelxp  4842  elvvv  4872  opabid2  4942  opeliunxp2  4951  elsnres  5119  elimasng  5172  dmsnopg  5286  cnvsng  5301  elsnxp  5357  funopg  5593  f1osng  5836  f1oprswap  5837  dmfco  5923  fvelrn  5999  fsng  6048  fprg  6058  fvrnressn  6064  fvsng  6083  funfvima3  6128  oveq1  6283  oprabid  6303  dfoprab2  6325  cbvoprab1  6351  elxp4  6725  elxp5  6726  opabex3d  6759  opabex3  6760  op1stg  6793  op2ndg  6794  el2xptp  6824  dfoprab4f  6839  frxp  6894  opeliunxp2f  6944  tfrlem11  7093  omeu  7273  oeeui  7290  elixpsn  7548  fundmen  7630  xpsnen  7643  xpassen  7653  xpf1o  7721  unxpdomlem1  7763  dfac5lem1  8541  dfac5lem4  8544  axdc4lem  8872  nqereu  9341  mulcanenq  9372  archnq  9392  prlem934  9445  supsrlem  9522  supsr  9523  swrdccatin1  12838  swrdccat3blem  12850  fsum2dlem  13842  fprod2dlem  14045  vdwlem10  14951  imasaddfnlem  15445  catideu  15592  iscatd2  15598  catlid  15600  catpropd  15625  symg2bas  17050  efgmval  17373  efgi  17380  vrgpval  17428  gsumcom2  17618  txkgen  20678  cnmpt21  20697  xkoinjcn  20713  txcon  20715  pt1hmeo  20832  cnextfvval  21091  qustgplem  21146  dvbsss  22869  axlowdim2  25002  axlowdim  25003  axcontlem10  25015  axcontlem12  25017  0eusgraiff0rgra  25679  drngoi  26147  isdivrngo  26171  isnvlem  26241  br8d  28227  cnvoprab  28316  prsrn  28728  esum2dlem  28920  eulerpartlemgvv  29215  br8  30402  br6  30403  br4  30404  eldm3  30408  br1steqg  30422  br2ndeqg  30423  dfdm5  30424  elfuns  30688  brimg  30710  brapply  30711  brsuccf  30714  brrestrict  30722  dfrdg4  30724  cgrdegen  30777  brofs  30778  cgrextend  30781  brifs  30816  ifscgr  30817  brcgr3  30819  brcolinear2  30831  colineardim1  30834  brfs  30852  idinside  30857  btwnconn1lem7  30866  btwnconn1lem11  30870  btwnconn1lem12  30871  brsegle  30881  outsideofeu  30904  fvray  30914  linedegen  30916  fvline  30917  bj-inftyexpiinv  31652  bj-inftyexpidisj  31654  finxpeq2  31781  finxpreclem6  31790  finxpsuclem  31791  dicelval3  34750  dihjatcclem4  34991  dropab1  36801  relopabVD  37295