MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opeq1 Structured version   Visualization version   GIF version

Theorem opeq1 4196
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
StepHypRef Expression
1 eleq1 2571 . . . 4 (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
21anbi1d 728 . . 3 (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3 sneq 4005 . . . 4 (𝐴 = 𝐵 → {𝐴} = {𝐵})
4 preq1 4079 . . . 4 (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
53, 4preq12d 4087 . . 3 (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
62, 5ifbieq1d 3931 . 2 (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7 dfopif 4193 . 2 𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8 dfopif 4193 . 2 𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
96, 7, 83eqtr4g 2564 1 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 378   = wceq 1468  wcel 1937  Vcvv 3066  c0 3757  ifcif 3908  {csn 3995  {cpr 3997  cop 4001
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-rab 2800  df-v 3068  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-sn 3996  df-pr 3998  df-op 4002
This theorem is referenced by:  opeq12  4198  opeq1i  4199  opeq1d  4202  oteq1  4205  breq1  4437  cbvopab1  4505  cbvopab1s  4507  opthg  4718  eqvinop  4727  opelopabsb  4752  opelxp  4910  elvvv  4941  opabid2  5011  opeliunxp2  5020  elsnres  5191  elimasng  5244  dmsnopg  5358  cnvsng  5373  elsnxp  5429  funopg  5665  f1osng  5913  f1oprswap  5916  dmfco  6006  fvelrn  6082  fsng  6131  fprg  6141  fvrnressn  6147  fvsng  6166  funfvima3  6213  oveq1  6370  oprabid  6390  dfoprab2  6412  cbvoprab1  6438  elxp4  6814  elxp5  6815  opabex3d  6848  opabex3  6849  op1stg  6882  op2ndg  6883  el2xptp  6913  dfoprab4f  6928  frxp  6985  opeliunxp2f  7034  tfrlem11  7183  omeu  7363  oeeui  7380  elixpsn  7644  fundmen  7727  xpsnen  7740  xpassen  7750  xpf1o  7818  unxpdomlem1  7860  dfac5lem1  8639  dfac5lem4  8642  axdc4lem  8970  nqereu  9439  mulcanenq  9470  archnq  9490  prlem934  9543  supsrlem  9620  supsr  9621  swrdccatin1  12972  swrdccat3blem  12984  fsum2dlem  13991  fprod2dlem  14194  vdwlem10  15102  imasaddfnlem  15599  catideu  15747  iscatd2  15753  catlid  15755  catpropd  15780  symg2bas  17200  efgmval  17523  efgi  17530  vrgpval  17578  gsumcom2  17768  txkgen  20824  cnmpt21  20843  xkoinjcn  20859  txcon  20861  pt1hmeo  20978  cnextfvval  21238  qustgplem  21293  dvbsss  23018  axlowdim2  25151  axlowdim  25152  axcontlem10  25164  axcontlem12  25166  0eusgraiff0rgra  25827  drngoi  26298  isdivrngo  26322  isnvlem  26392  br8d  28376  cnvoprab  28464  prsrn  28876  esum2dlem  29068  eulerpartlemgvv  29363  br8  30547  br6  30548  br4  30549  eldm3  30553  br1steqg  30567  br2ndeqg  30568  dfdm5  30569  elfuns  30833  brimg  30855  brapply  30856  brsuccf  30859  brrestrict  30867  dfrdg4  30869  cgrdegen  30922  brofs  30923  cgrextend  30926  brifs  30961  ifscgr  30962  brcgr3  30964  brcolinear2  30976  colineardim1  30979  brfs  30997  idinside  31002  btwnconn1lem7  31011  btwnconn1lem11  31015  btwnconn1lem12  31016  brsegle  31026  outsideofeu  31049  fvray  31059  linedegen  31061  fvline  31062  bj-inftyexpiinv  31871  bj-inftyexpidisj  31873  finxpeq2  32000  finxpreclem6  32009  finxpsuclem  32010  curfv  32158  dicelval3  34988  dihjatcclem4  35229  dropab1  37157  relopabVD  37646
  Copyright terms: Public domain W3C validator