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

Theorem opeq2 4796
Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
opeq2 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Proof of Theorem opeq2
StepHypRef Expression
1 eleq1 2897 . . . 4 (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
21anbi2d 628 . . 3 (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3 preq2 4662 . . . 4 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
43preq2d 4668 . . 3 (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
52, 4ifbieq1d 4486 . 2 (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6 dfopif 4792 . 2 𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7 dfopif 4792 . 2 𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
85, 6, 73eqtr4g 2878 1 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  Vcvv 3492  c0 4288  ifcif 4463  {csn 4557  {cpr 4559  cop 4563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564
This theorem is referenced by:  opeq12  4797  opeq2i  4799  opeq2d  4802  oteq2  4805  oteq3  4806  breq2  5061  cbvopab2  5132  cbvopab2v  5135  opthg  5360  eqvinop  5369  opelopabsb  5408  dfid3  5455  opelxp  5584  relopabi  5687  opabid2  5693  elrn2g  5754  opeldmd  5768  opeldm  5769  elrn2  5814  iss  5896  elidinxp  5904  elimasng  5948  dmsnopg  6063  reuop  6137  funopg  6382  f1osng  6648  f1oprswap  6651  tz6.12f  6687  fvn0ssdmfun  6834  fsn  6889  fsng  6891  fprg  6909  fprb  6948  oveq2  7153  cbvoprab2  7231  ovg  7302  elxp4  7616  elxp5  7617  opabex3d  7655  opabex3rd  7656  opabex3  7657  op1stg  7690  op2ndg  7691  op1steq  7722  dfoprab4f  7743  fsplit  7801  seqomlem2  8076  omeu  8200  oeeui  8217  ralxpmap  8448  elixpsn  8489  ixpsnf1o  8490  mapsnend  8576  xpsnen  8589  xpassen  8599  xpf1o  8667  unxpdomlem1  8710  djulcl  9327  djurcl  9328  djur  9336  djuss  9337  djuun  9343  1stinl  9344  2ndinl  9345  1stinr  9346  2ndinr  9347  axdc4lem  9865  nqereu  10339  mulcanenq  10370  elreal  10541  ax1rid  10571  fseq1p1m1  12969  pfxval  14023  swrdccatin1  14075  swrdccat3blem  14089  wrdlen2  14294  ruclem1  15572  imasaddfnlem  16789  imasvscafn  16798  catidex  16933  catpropd  16967  funcsetcestrclem1  17392  symg2bas  18455  efgi  18774  gsumcom2  19024  mat1rhmval  21016  mat1ric  21024  txkgen  22188  cnmpt21  22207  xkoinjcn  22223  txconn  22225  xpstopnlem1  22345  qustgplem  22656  metustid  23091  axlowdim2  26673  axlowdim  26674  axcontlem2  26678  axcontlem3  26679  axcontlem4  26680  axcontlem9  26685  axcontlem10  26686  axcontlem11  26687  cusgrexg  27153  rgrusgrprc  27298  2clwwlk2clwwlk  28056  isnvlem  28314  br8d  30289  prsdm  31056  eulerpartlemgvv  31533  reprsuc  31785  bnj941  31943  bnj944  32109  cvmlift2lem1  32446  cvmlift2lem12  32458  goel  32491  gonafv  32494  satf0op  32521  sat1el2xp  32523  fmla0xp  32527  sategoelfvb  32563  br8  32889  br6  32890  br4  32891  dfrn5  32914  elima4  32916  pprodss4v  33242  brimg  33295  brapply  33296  brsuccf  33299  brrestrict  33307  dfrdg4  33309  cgrtriv  33360  brofs  33363  segconeu  33369  btwntriv2  33370  transportprops  33392  brifs  33401  ifscgr  33402  brcgr3  33404  cgrxfr  33413  brcolinear2  33416  colineardim1  33419  brfs  33437  idinside  33442  btwnconn1lem7  33451  btwnconn1lem11  33455  btwnconn1lem12  33456  btwnconn1lem14  33458  brsegle  33466  seglerflx  33470  seglemin  33471  segleantisym  33473  btwnsegle  33475  outsideofeu  33489  outsidele  33490  linedegen  33501  fvline  33502  finxpreclem6  34559  finxpsuclem  34560  curfv  34753  poimirlem4  34777  poimirlem26  34799  isdivrngo  35109  drngoi  35110  iss2  35482  dibelval3  38163  diblsmopel  38187  dihjatcclem4  38437  frlmsnic  39027  dfhe3  39999  dffrege115  40202  dropab2  40657  relopabVD  41112  projf1o  41335  sge0xp  42588  hoidmv1le  42753  ichnreuop  43511  ichreuopeq  43512  reuopreuprim  43565  prelrrx2b  44629  rrx2xpref1o  44633  rrx2plordisom  44638
  Copyright terms: Public domain W3C validator