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

Theorem opeq1 4340
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 2676 . . . 4 (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
21anbi1d 737 . . 3 (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3 sneq 4135 . . . 4 (𝐴 = 𝐵 → {𝐴} = {𝐵})
4 preq1 4212 . . . 4 (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
53, 4preq12d 4220 . . 3 (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
62, 5ifbieq1d 4059 . 2 (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7 dfopif 4337 . 2 𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8 dfopif 4337 . 2 𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
96, 7, 83eqtr4g 2669 1 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1475  wcel 1977  Vcvv 3173  c0 3874  ifcif 4036  {csn 4125  {cpr 4127  cop 4131
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132
This theorem is referenced by:  opeq12  4342  opeq1i  4343  opeq1d  4346  oteq1  4349  breq1  4586  cbvopab1  4655  cbvopab1s  4657  opthg  4872  eqvinop  4881  opelopabsb  4910  opelxp  5070  elvvv  5101  opabid2  5173  opeliunxp2  5182  elsnres  5356  elimasng  5410  dmsnopg  5524  cnvsng  5539  elsnxpOLD  5595  funopg  5836  f1osng  6089  f1oprswap  6092  dmfco  6182  fvelrn  6260  fsng  6310  fprg  6327  fvrnressn  6333  fvsng  6352  funfvima3  6399  oveq1  6556  oprabid  6576  dfoprab2  6599  cbvoprab1  6625  elxp4  7003  elxp5  7004  opabex3d  7037  opabex3  7038  op1stg  7071  op2ndg  7072  el2xptp  7102  dfoprab4f  7117  frxp  7174  opeliunxp2f  7223  tfrlem11  7371  omeu  7552  oeeui  7569  elixpsn  7833  fundmen  7916  xpsnen  7929  xpassen  7939  xpf1o  8007  unxpdomlem1  8049  dfac5lem1  8829  dfac5lem4  8832  axdc4lem  9160  nqereu  9630  mulcanenq  9661  archnq  9681  prlem934  9734  supsrlem  9811  supsr  9812  swrdccatin1  13334  swrdccat3blem  13346  fsum2dlem  14343  fprod2dlem  14549  vdwlem10  15532  imasaddfnlem  16011  catideu  16159  iscatd2  16165  catlid  16167  catpropd  16192  symg2bas  17641  efgmval  17948  efgi  17955  vrgpval  18003  gsumcom2  18197  txkgen  21265  cnmpt21  21284  xkoinjcn  21300  txcon  21302  pt1hmeo  21419  cnextfvval  21679  qustgplem  21734  dvbsss  23472  axlowdim2  25640  axlowdim  25641  axcontlem10  25653  axcontlem12  25655  0eusgraiff0rgra  26466  isnvlem  26849  br8d  28802  cnvoprab  28886  prsrn  29289  esum2dlem  29481  eulerpartlemgvv  29765  br8  30899  br6  30900  br4  30901  eldm3  30905  br1steqg  30919  br2ndeqg  30920  dfdm5  30921  elfuns  31192  brimg  31214  brapply  31215  brsuccf  31218  brrestrict  31226  dfrdg4  31228  cgrdegen  31281  brofs  31282  cgrextend  31285  brifs  31320  ifscgr  31321  brcgr3  31323  brcolinear2  31335  colineardim1  31338  brfs  31356  idinside  31361  btwnconn1lem7  31370  btwnconn1lem11  31374  btwnconn1lem12  31375  brsegle  31385  outsideofeu  31408  fvray  31418  linedegen  31420  fvline  31421  bj-inftyexpiinv  32272  bj-inftyexpidisj  32274  finxpeq2  32400  finxpreclem6  32409  finxpsuclem  32410  curfv  32559  isdivrngo  32919  drngoi  32920  dicelval3  35487  dihjatcclem4  35728  dropab1  37672  relopabVD  38159
  Copyright terms: Public domain W3C validator