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

Theorem opeq2 4596
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 2873 . . . 4 (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
21anbi2d 616 . . 3 (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3 preq2 4460 . . . 4 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
43preq2d 4466 . . 3 (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
52, 4ifbieq1d 4302 . 2 (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6 dfopif 4592 . 2 𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7 dfopif 4592 . 2 𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
85, 6, 73eqtr4g 2865 1 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1637  wcel 2156  Vcvv 3391  c0 4116  ifcif 4279  {csn 4370  {cpr 4372  cop 4376
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377
This theorem is referenced by:  opeq12  4597  opeq2i  4599  opeq2d  4602  oteq2  4605  oteq3  4606  breq2  4848  cbvopab2  4918  cbvopab2v  4921  opthg  5135  eqvinop  5144  opelopabsb  5180  dfid3  5220  opelxp  5346  relopabi  5447  opabid2  5453  elrn2g  5514  opeldmd  5528  opeldm  5529  elrn2  5566  opelresgOLD  5609  iss  5652  elidinxp  5660  elridOLD  5663  elimasng  5701  idrefOLD  5720  dmsnopg  5818  cnvsngOLD  5835  funopg  6131  f1osng  6389  f1oprswap  6392  tz6.12f  6428  fvn0ssdmfun  6568  fsn  6621  fsng  6623  funsneqopsnOLD  6637  fprg  6642  fvsng  6668  oveq2  6878  cbvoprab2  6954  ovg  7025  elxp4  7336  elxp5  7337  opabex3d  7371  opabex3  7372  op1stg  7406  op2ndg  7407  op1steq  7438  dfoprab4f  7454  seqomlem2  7778  omeu  7898  oeeui  7915  ralxpmap  8140  elixpsn  8180  ixpsnf1o  8181  mapsnend  8267  xpsnen  8279  xpassen  8289  xpf1o  8357  unxpdomlem1  8399  djulcl  9015  djurcl  9016  djur  9024  djuss  9025  djuun  9031  1stinl  9032  2ndinl  9033  1stinr  9034  2ndinr  9035  axdc4lem  9558  nqereu  10032  mulcanenq  10063  elreal  10233  ax1rid  10263  fseq1p1m1  12633  swrdccatin1  13703  swrdccat3blem  13715  swrdccatid  13717  swrdccatin12d  13721  wrdlen2  13909  ruclem1  15176  imasaddfnlem  16389  imasvscafn  16398  catidex  16535  catpropd  16569  funcsetcestrclem1  16995  symg2bas  18015  psgnunilem5  18111  efgi  18329  gsumcom2  18571  mat1rhmval  20493  mat1ric  20501  txkgen  21666  cnmpt21  21685  xkoinjcn  21701  txconn  21703  xpstopnlem1  21823  qustgplem  22134  metustid  22569  axlowdim2  26053  axlowdim  26054  axcontlem2  26058  axcontlem3  26059  axcontlem4  26060  axcontlem9  26065  axcontlem10  26066  axcontlem11  26067  cusgrexg  26567  rgrusgrprc  26712  wwlksnextbi  27030  wwlksnextinj  27035  wwlksnextsur  27036  clwwlkfo  27198  clwlksfclwwlkOLD  27235  2clwwlk2clwwlk  27526  isnvlem  27792  br8d  29746  prsdm  30284  eulerpartlemgvv  30762  reprsuc  31017  bnj941  31164  bnj944  31329  cvmlift2lem1  31605  cvmlift2lem12  31617  br8  31966  br6  31967  br4  31968  fprb  31989  br1steqgOLD  31992  br2ndeqgOLD  31993  dfrn5  31995  elima4  31997  pprodss4v  32310  brimg  32363  brapply  32364  brsuccf  32367  brrestrict  32375  dfrdg4  32377  cgrtriv  32428  brofs  32431  segconeu  32437  btwntriv2  32438  transportprops  32460  brifs  32469  ifscgr  32470  brcgr3  32472  cgrxfr  32481  brcolinear2  32484  colineardim1  32487  brfs  32505  idinside  32510  btwnconn1lem7  32519  btwnconn1lem11  32523  btwnconn1lem12  32524  btwnconn1lem14  32526  brsegle  32534  seglerflx  32538  seglemin  32539  segleantisym  32541  btwnsegle  32543  outsideofeu  32557  outsidele  32558  linedegen  32569  fvline  32570  finxpreclem6  33547  finxpsuclem  33548  curfv  33700  poimirlem4  33724  poimirlem26  33746  isdivrngo  34058  drngoi  34059  iss2  34423  dibelval3  36925  diblsmopel  36949  dihjatcclem4  37199  dfhe3  38566  dffrege115  38769  dropab2  39147  relopabVD  39628  projf1o  39872  sge0xp  41122  hoidmv1le  41287  pfxval  41955
  Copyright terms: Public domain W3C validator