Theorem opeq1 4817

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

Assertion

Ref	Expression
opeq1	⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Proof of Theorem opeq1

Step	Hyp	Ref	Expression
1		eleq1 2825	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 632	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4578	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4678	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4686	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4492	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4814	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4814	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2797	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3430  ∅c0 4274  ifcif 4467  {csn 4568  {cpr 4570  ⟨cop 4574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575

This theorem is referenced by:  opeq12  4819  opeq1i  4820  opeq1d  4823  oteq1  4826  breq1  5089  cbvopab1  5160  cbvopab1g  5161  cbvopab1s  5163  cbvopab1v  5164  opthg  5425  eqvinop  5435  sbcop1  5436  opelopabsb  5478  opelxp  5660  elvvv  5700  opabid2  5777  opeliunxp2  5787  elsnres  5980  dmsnopg  6171  reuop  6251  funopg  6526  f1osng  6816  f1oprswap  6819  dmfco  6930  fvelrn  7022  fsng  7084  funsneqopb  7099  fprg  7102  fvrnressn  7108  funfvima3  7184  oveq1  7367  oprabidw  7391  oprabid  7392  dfoprab2  7418  cbvoprab1  7447  elxp4  7866  elxp5  7867  opabex3d  7911  opabex3rd  7912  opabex3  7913  op1stg  7947  op2ndg  7948  el2xptp  7981  dfoprab4f  8002  frxp  8069  frxp2  8087  xpord2pred  8088  opeliunxp2f  8153  tfrlem11  8320  omeu  8513  oeeui  8531  elixpsn  8878  fundmen  8971  xpsnen  8992  xpassen  9002  xpf1o  9070  unxpdomlem1  9159  djur  9834  dfac5lem1  10036  dfac5lem4  10039  dfac5lem4OLD  10041  axdc4lem  10368  nqereu  10843  mulcanenq  10874  archnq  10894  prlem934  10947  supsrlem  11025  supsr  11026  swrdccatin1  14678  swrdccat3blem  14692  fsum2dlem  15723  fprod2dlem  15936  vdwlem10  16952  imasaddfnlem  17483  catideu  17632  iscatd2  17638  catlid  17640  catpropd  17666  symg2bas  19359  efgmval  19678  efgi  19685  vrgpval  19733  gsumcom2  19941  rngqiprngimfo  21291  pzriprnglem10  21480  pzriprnglem11  21481  txkgen  23627  cnmpt21  23646  xkoinjcn  23662  txconn  23664  pt1hmeo  23781  cnextfvval  24040  qustgplem  24096  dvbsss  25879  axlowdim2  29043  axlowdim  29044  axcontlem10  29056  axcontlem12  29058  isnvlem  30696  br8d  32696  2ndresdju  32737  gsumhashmul  33143  gsumwrd2dccatlem  33153  rlocf1  33349  idomsubr  33385  prsrn  34075  esum2dlem  34252  eulerpartlemgvv  34536  fineqvrep  35274  satf0op  35575  satffunlem1lem1  35600  satffunlem2lem1  35602  sategoelfvb  35617  br8  35954  br6  35955  br4  35956  eldm3  35959  dfdm5  35971  elfuns  36111  brimg  36133  brapply  36134  lemsuccf  36137  brrestrict  36147  dfrdg4  36149  cgrdegen  36202  brofs  36203  cgrextend  36206  brifs  36241  ifscgr  36242  brcgr3  36244  brcolinear2  36256  colineardim1  36259  brfs  36277  idinside  36282  btwnconn1lem7  36291  btwnconn1lem11  36295  btwnconn1lem12  36296  brsegle  36306  outsideofeu  36329  fvray  36339  linedegen  36341  fvline  36342  cbvoprab1vw  36435  cbvoprab13vw  36439  cbvopab1davw  36462  cbvoprab1davw  36469  bj-inftyexpiinv  37538  bj-inftyexpidisj  37540  finxpeq2  37717  finxpreclem6  37726  finxpsuclem  37727  curfv  37935  isdivrngo  38285  drngoi  38286  dicelval3  41640  dihjatcclem4  41881  dropab1  44891  relopabVD  45345  funressndmafv2rn  47683  dfatdmfcoafv2  47714  ichnreuop  47944  ichreuopeq  47945  reuopreuprim  47998  gpgedgvtx0  48549  gpgedgvtx1  48550  gpgcubic  48567  gpg5nbgr3star  48569  pgnbgreunbgrlem3  48606  pgnbgreunbgrlem6  48612  pgnbgreunbgr  48613  sectpropdlem  49523  ssccatid  49559  upfval2  49664  isthincd2lem2  49922