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

Theorem opeq1 4238
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 2580 . . . 4 (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
21anbi1d 736 . . 3 (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3 sneq 4038 . . . 4 (𝐴 = 𝐵 → {𝐴} = {𝐵})
4 preq1 4115 . . . 4 (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
53, 4preq12d 4123 . . 3 (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
62, 5ifbieq1d 3962 . 2 (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7 dfopif 4235 . 2 𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8 dfopif 4235 . 2 𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
96, 7, 83eqtr4g 2573 1 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1938  Vcvv 3077  c0 3777  ifcif 3939  {csn 4028  {cpr 4030  cop 4034
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-rab 2809  df-v 3079  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035
This theorem is referenced by:  opeq12  4240  opeq1i  4241  opeq1d  4244  oteq1  4247  breq1  4484  cbvopab1  4553  cbvopab1s  4555  opthg  4770  eqvinop  4779  opelopabsb  4804  opelxp  4964  elvvv  4995  opabid2  5065  opeliunxp2  5074  elsnres  5247  elimasng  5301  dmsnopg  5414  cnvsng  5429  elsnxpOLD  5485  funopg  5721  f1osng  5972  f1oprswap  5975  dmfco  6065  fvelrn  6143  fsng  6193  fprg  6203  fvrnressn  6209  fvsng  6228  funfvima3  6275  oveq1  6432  oprabid  6452  dfoprab2  6475  cbvoprab1  6501  elxp4  6877  elxp5  6878  opabex3d  6911  opabex3  6912  op1stg  6945  op2ndg  6946  el2xptp  6976  dfoprab4f  6991  frxp  7048  opeliunxp2f  7097  tfrlem11  7246  omeu  7427  oeeui  7444  elixpsn  7708  fundmen  7791  xpsnen  7804  xpassen  7814  xpf1o  7882  unxpdomlem1  7924  dfac5lem1  8704  dfac5lem4  8707  axdc4lem  9035  nqereu  9505  mulcanenq  9536  archnq  9556  prlem934  9609  supsrlem  9686  supsr  9687  swrdccatin1  13191  swrdccat3blem  13203  fsum2dlem  14210  fprod2dlem  14416  vdwlem10  15414  imasaddfnlem  15901  catideu  16049  iscatd2  16055  catlid  16057  catpropd  16082  symg2bas  17531  efgmval  17854  efgi  17861  vrgpval  17909  gsumcom2  18102  txkgen  21166  cnmpt21  21185  xkoinjcn  21201  txcon  21203  pt1hmeo  21320  cnextfvval  21580  qustgplem  21635  dvbsss  23348  axlowdim2  25531  axlowdim  25532  axcontlem10  25544  axcontlem12  25546  0eusgraiff0rgra  26205  isnvlem  26606  br8d  28591  cnvoprab  28675  prsrn  29086  esum2dlem  29278  eulerpartlemgvv  29573  br8  30742  br6  30743  br4  30744  eldm3  30748  br1steqg  30762  br2ndeqg  30763  dfdm5  30764  elfuns  31028  brimg  31050  brapply  31051  brsuccf  31054  brrestrict  31062  dfrdg4  31064  cgrdegen  31117  brofs  31118  cgrextend  31121  brifs  31156  ifscgr  31157  brcgr3  31159  brcolinear2  31171  colineardim1  31174  brfs  31192  idinside  31197  btwnconn1lem7  31206  btwnconn1lem11  31210  btwnconn1lem12  31211  brsegle  31221  outsideofeu  31244  fvray  31254  linedegen  31256  fvline  31257  bj-inftyexpiinv  32104  bj-inftyexpidisj  32106  finxpeq2  32232  finxpreclem6  32241  finxpsuclem  32242  curfv  32434  isdivrngo  32794  drngoi  32795  dicelval3  35362  dihjatcclem4  35603  dropab1  37554  relopabVD  38041
  Copyright terms: Public domain W3C validator