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

Theorem opeq1 4795
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 2897 . . . 4 (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
21anbi1d 629 . . 3 (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3 sneq 4567 . . . 4 (𝐴 = 𝐵 → {𝐴} = {𝐵})
4 preq1 4661 . . . 4 (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
53, 4preq12d 4669 . . 3 (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
62, 5ifbieq1d 4486 . 2 (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7 dfopif 4792 . 2 𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8 dfopif 4792 . 2 𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
96, 7, 83eqtr4g 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  opeq1i  4798  opeq1d  4801  oteq1  4804  breq1  5060  cbvopab1  5130  cbvopab1g  5131  cbvopab1s  5133  opthg  5360  eqvinop  5369  sbcop1  5370  opelopabsb  5408  opelxp  5584  elvvv  5620  opabid2  5693  opeliunxp2  5702  elsnres  5885  elimasng  5948  dmsnopg  6063  reuop  6137  funopg  6382  f1osng  6648  f1oprswap  6651  dmfco  6750  fvelrn  6836  fsng  6891  funsneqopb  6906  fprg  6909  fvrnressn  6915  funfvima3  6989  oveq1  7152  oprabidw  7176  oprabid  7177  dfoprab2  7201  cbvoprab1  7230  elxp4  7616  elxp5  7617  opabex3d  7655  opabex3rd  7656  opabex3  7657  op1stg  7690  op2ndg  7691  el2xptp  7724  dfoprab4f  7743  frxp  7809  opeliunxp2f  7865  tfrlem11  8013  omeu  8200  oeeui  8217  elixpsn  8489  fundmen  8571  xpsnen  8589  xpassen  8599  xpf1o  8667  unxpdomlem1  8710  djur  9336  dfac5lem1  9537  dfac5lem4  9540  axdc4lem  9865  nqereu  10339  mulcanenq  10370  archnq  10390  prlem934  10443  supsrlem  10521  supsr  10522  swrdccatin1  14075  swrdccat3blem  14089  fsum2dlem  15113  fprod2dlem  15322  vdwlem10  16314  imasaddfnlem  16789  catideu  16934  iscatd2  16940  catlid  16942  catpropd  16967  symg2bas  18455  efgmval  18767  efgi  18774  vrgpval  18822  gsumcom2  19024  txkgen  22188  cnmpt21  22207  xkoinjcn  22223  txconn  22225  pt1hmeo  22342  cnextfvval  22601  qustgplem  22656  dvbsss  24427  axlowdim2  26673  axlowdim  26674  axcontlem10  26686  axcontlem12  26688  isnvlem  28314  br8d  30289  cnvoprabOLD  30382  prsrn  31057  esum2dlem  31250  eulerpartlemgvv  31533  satf0op  32521  satffunlem1lem1  32546  satffunlem2lem1  32548  sategoelfvb  32563  br8  32889  br6  32890  br4  32891  eldm3  32894  dfdm5  32913  elfuns  33273  brimg  33295  brapply  33296  brsuccf  33299  brrestrict  33307  dfrdg4  33309  cgrdegen  33362  brofs  33363  cgrextend  33366  brifs  33401  ifscgr  33402  brcgr3  33404  brcolinear2  33416  colineardim1  33419  brfs  33437  idinside  33442  btwnconn1lem7  33451  btwnconn1lem11  33455  btwnconn1lem12  33456  brsegle  33466  outsideofeu  33489  fvray  33499  linedegen  33501  fvline  33502  bj-inftyexpiinv  34382  bj-inftyexpidisj  34384  finxpeq2  34550  finxpreclem6  34559  finxpsuclem  34560  curfv  34753  isdivrngo  35109  drngoi  35110  dicelval3  38196  dihjatcclem4  38437  dropab1  40656  relopabVD  41112  funressndmafv2rn  43299  dfatdmfcoafv2  43330  ichnreuop  43511  ichreuopeq  43512  reuopreuprim  43565
  Copyright terms: Public domain W3C validator