Theorem opeq1 4187

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 2495	. . . 4 |- ( A = B -> ( A e. _V <-> B e. _V ) )
2	1	anbi1d 709	. . 3 |- ( A = B -> ( ( A e. _V /\ C e. _V ) <-> ( B e. _V /\ C e. _V ) ) )
3		sneq 4008	. . . 4 |- ( A = B -> { A } = { B } )
4		preq1 4079	. . . 4 |- ( A = B -> { A , C } = { B , C } )
5	3, 4	preq12d 4087	. . 3 |- ( A = B -> { { A } , { A , C } } = { { B } , { B , C } } )
6	2, 5	ifbieq1d 3934	. 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 4184	. 2 |- <. A , C >. = if ( ( A e. _V /\ C e. _V ) , { { A } , { A , C } } , (/) )
8		dfopif 4184	. 2 |- <. B , C >. = if ( ( B e. _V /\ C e. _V ) , { { B } , { B , C } } , (/) )
9	6, 7, 8	3eqtr4g 2488	1 |- ( A = B -> <. A , C >. = <. B , C >. )

Syntax hints:   -> wi 4   /\ wa 370   = wceq 1437   e. wcel 1872   _Vcvv 3080   (/)c0 3761   ifcif 3911   {csn 3998   {cpr 4000   <.cop 4004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005

This theorem is referenced by:  opeq12  4189  opeq1i  4190  opeq1d  4193  oteq1  4196  breq1  4426  cbvopab1  4494  cbvopab1s  4496  opthg  4696  eqvinop  4705  opelopabsb  4730  opelxp  4883  elvvv  4913  opabid2  4983  opeliunxp2  4992  elsnres  5160  elimasng  5213  dmsnopg  5326  cnvsng  5341  elsnxp  5397  funopg  5633  f1osng  5869  f1oprswap  5870  dmfco  5955  fvelrn  6030  fsng  6078  fprg  6088  fvrnressn  6094  fvsng  6113  funfvima3  6157  oveq1  6312  oprabid  6332  dfoprab2  6351  cbvoprab1  6377  elxp4  6751  elxp5  6752  opabex3d  6785  opabex3  6786  op1stg  6819  op2ndg  6820  el2xptp  6850  dfoprab4f  6865  frxp  6917  opeliunxp2f  6967  tfrlem11  7117  omeu  7297  oeeui  7314  elixpsn  7572  fundmen  7653  xpsnen  7665  xpassen  7675  xpf1o  7743  unxpdomlem1  7785  dfac5lem1  8561  dfac5lem4  8564  axdc4lem  8892  nqereu  9361  mulcanenq  9392  archnq  9412  prlem934  9465  supsrlem  9542  supsr  9543  swrdccatin1  12841  swrdccat3blem  12853  fsum2dlem  13830  fprod2dlem  14033  vdwlem10  14939  imasaddfnlem  15433  catideu  15580  iscatd2  15586  catlid  15588  catpropd  15613  symg2bas  17038  efgmval  17361  efgi  17368  vrgpval  17416  gsumcom2  17606  txkgen  20665  cnmpt21  20684  xkoinjcn  20700  txcon  20702  pt1hmeo  20819  cnextfvval  21078  qustgplem  21133  dvbsss  22855  axlowdim2  24988  axlowdim  24989  axcontlem10  25001  axcontlem12  25003  0eusgraiff0rgra  25665  drngoi  26133  isdivrngo  26157  isnvlem  26227  br8d  28220  cnvoprab  28314  prsrn  28729  esum2dlem  28921  eulerpartlemgvv  29217  br8  30403  br6  30404  br4  30405  eldm3  30409  br1steqg  30423  br2ndeqg  30424  dfdm5  30425  elfuns  30687  brimg  30709  brapply  30710  brsuccf  30713  brrestrict  30721  dfrdg4  30723  cgrdegen  30776  brofs  30777  cgrextend  30780  brifs  30815  ifscgr  30816  brcgr3  30818  brcolinear2  30830  colineardim1  30833  brfs  30851  idinside  30856  btwnconn1lem7  30865  btwnconn1lem11  30869  btwnconn1lem12  30870  brsegle  30880  outsideofeu  30903  fvray  30913  linedegen  30915  fvline  30916  bj-inftyexpiinv  31614  bj-inftyexpidisj  31616  finxpeq2  31743  finxpreclem6  31752  finxpsuclem  31753  dicelval3  34717  dihjatcclem4  34958  dropab1  36770  relopabVD  37271