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

Theorem opeq1 4539
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 2838 . . . 4 (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
21anbi1d 615 . . 3 (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3 sneq 4326 . . . 4 (𝐴 = 𝐵 → {𝐴} = {𝐵})
4 preq1 4404 . . . 4 (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
53, 4preq12d 4412 . . 3 (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
62, 5ifbieq1d 4248 . 2 (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7 dfopif 4536 . 2 𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8 dfopif 4536 . 2 𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
96, 7, 83eqtr4g 2830 1 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1631  wcel 2145  Vcvv 3351  c0 4063  ifcif 4225  {csn 4316  {cpr 4318  cop 4322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323
This theorem is referenced by:  opeq12  4541  opeq1i  4542  opeq1d  4545  oteq1  4548  breq1  4789  cbvopab1  4857  cbvopab1s  4859  opthg  5073  eqvinop  5082  opelopabsb  5118  opelxp  5286  elvvv  5318  opabid2  5390  opeliunxp2  5399  elsnres  5577  elimasng  5632  dmsnopg  5748  cnvsngOLD  5765  funopg  6065  f1osng  6318  f1oprswap  6321  dmfco  6414  fvelrn  6495  fsng  6547  funsneqopb  6562  fprg  6565  fvrnressn  6571  fvsng  6591  funfvima3  6638  oveq1  6800  oprabid  6822  dfoprab2  6848  cbvoprab1  6874  elxp4  7257  elxp5  7258  opabex3d  7292  opabex3  7293  op1stg  7327  op2ndg  7328  el2xptp  7360  dfoprab4f  7375  frxp  7438  opeliunxp2f  7488  tfrlem11  7637  omeu  7819  oeeui  7836  elixpsn  8101  fundmen  8183  xpsnen  8200  xpassen  8210  xpf1o  8278  unxpdomlem1  8320  djur  8945  dfac5lem1  9146  dfac5lem4  9149  axdc4lem  9479  nqereu  9953  mulcanenq  9984  archnq  10004  prlem934  10057  supsrlem  10134  supsr  10135  swrdccatin1  13692  swrdccat3blem  13704  fsum2dlem  14709  fprod2dlem  14917  vdwlem10  15901  imasaddfnlem  16396  catideu  16543  iscatd2  16549  catlid  16551  catpropd  16576  symg2bas  18025  efgmval  18332  efgi  18339  vrgpval  18387  gsumcom2  18581  txkgen  21676  cnmpt21  21695  xkoinjcn  21711  txconn  21713  pt1hmeo  21830  cnextfvval  22089  qustgplem  22144  dvbsss  23886  axlowdim2  26061  axlowdim  26062  axcontlem10  26074  axcontlem12  26076  isnvlem  27805  br8d  29760  cnvoprabOLD  29838  prsrn  30301  esum2dlem  30494  eulerpartlemgvv  30778  br8  31984  br6  31985  br4  31986  eldm3  31989  br1steqgOLD  32010  br2ndeqgOLD  32011  dfdm5  32012  elfuns  32359  brimg  32381  brapply  32382  brsuccf  32385  brrestrict  32393  dfrdg4  32395  cgrdegen  32448  brofs  32449  cgrextend  32452  brifs  32487  ifscgr  32488  brcgr3  32490  brcolinear2  32502  colineardim1  32505  brfs  32523  idinside  32528  btwnconn1lem7  32537  btwnconn1lem11  32541  btwnconn1lem12  32542  brsegle  32552  outsideofeu  32575  fvray  32585  linedegen  32587  fvline  32588  bj-inftyexpiinv  33432  bj-inftyexpidisj  33434  finxpeq2  33561  finxpreclem6  33570  finxpsuclem  33571  curfv  33722  isdivrngo  34081  drngoi  34082  dicelval3  36990  dihjatcclem4  37231  dropab1  39176  relopabVD  39659
  Copyright terms: Public domain W3C validator