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

Theorem opeq1 4333
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 2674 . . . 4 (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
21anbi1d 736 . . 3 (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3 sneq 4133 . . . 4 (𝐴 = 𝐵 → {𝐴} = {𝐵})
4 preq1 4210 . . . 4 (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
53, 4preq12d 4218 . . 3 (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
62, 5ifbieq1d 4057 . 2 (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7 dfopif 4330 . 2 𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8 dfopif 4330 . 2 𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
96, 7, 83eqtr4g 2667 1 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1976  Vcvv 3171  c0 3872  ifcif 4034  {csn 4123  {cpr 4125  cop 4129
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2588
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 1700  df-sb 1867  df-clab 2595  df-cleq 2601  df-clel 2604  df-nfc 2738  df-rab 2903  df-v 3173  df-dif 3541  df-un 3543  df-in 3545  df-ss 3552  df-nul 3873  df-if 4035  df-sn 4124  df-pr 4126  df-op 4130
This theorem is referenced by:  opeq12  4335  opeq1i  4336  opeq1d  4339  oteq1  4342  breq1  4579  cbvopab1  4648  cbvopab1s  4650  opthg  4865  eqvinop  4874  opelopabsb  4899  opelxp  5059  elvvv  5090  opabid2  5160  opeliunxp2  5169  elsnres  5342  elimasng  5396  dmsnopg  5509  cnvsng  5524  elsnxpOLD  5580  funopg  5821  f1osng  6073  f1oprswap  6076  dmfco  6166  fvelrn  6244  fsng  6294  fprg  6304  fvrnressn  6310  fvsng  6329  funfvima3  6376  oveq1  6533  oprabid  6553  dfoprab2  6576  cbvoprab1  6602  elxp4  6979  elxp5  6980  opabex3d  7013  opabex3  7014  op1stg  7047  op2ndg  7048  el2xptp  7078  dfoprab4f  7093  frxp  7150  opeliunxp2f  7199  tfrlem11  7347  omeu  7528  oeeui  7545  elixpsn  7809  fundmen  7892  xpsnen  7905  xpassen  7915  xpf1o  7983  unxpdomlem1  8025  dfac5lem1  8805  dfac5lem4  8808  axdc4lem  9136  nqereu  9606  mulcanenq  9637  archnq  9657  prlem934  9710  supsrlem  9787  supsr  9788  swrdccatin1  13279  swrdccat3blem  13291  fsum2dlem  14288  fprod2dlem  14494  vdwlem10  15477  imasaddfnlem  15956  catideu  16104  iscatd2  16110  catlid  16112  catpropd  16137  symg2bas  17586  efgmval  17893  efgi  17900  vrgpval  17948  gsumcom2  18142  txkgen  21206  cnmpt21  21225  xkoinjcn  21241  txcon  21243  pt1hmeo  21360  cnextfvval  21620  qustgplem  21675  dvbsss  23388  axlowdim2  25557  axlowdim  25558  axcontlem10  25570  axcontlem12  25572  0eusgraiff0rgra  26231  isnvlem  26632  br8d  28607  cnvoprab  28691  prsrn  29094  esum2dlem  29286  eulerpartlemgvv  29570  br8  30704  br6  30705  br4  30706  eldm3  30710  br1steqg  30724  br2ndeqg  30725  dfdm5  30726  elfuns  30997  brimg  31019  brapply  31020  brsuccf  31023  brrestrict  31031  dfrdg4  31033  cgrdegen  31086  brofs  31087  cgrextend  31090  brifs  31125  ifscgr  31126  brcgr3  31128  brcolinear2  31140  colineardim1  31143  brfs  31161  idinside  31166  btwnconn1lem7  31175  btwnconn1lem11  31179  btwnconn1lem12  31180  brsegle  31190  outsideofeu  31213  fvray  31223  linedegen  31225  fvline  31226  bj-inftyexpiinv  32074  bj-inftyexpidisj  32076  finxpeq2  32202  finxpreclem6  32211  finxpsuclem  32212  curfv  32361  isdivrngo  32721  drngoi  32722  dicelval3  35289  dihjatcclem4  35530  dropab1  37474  relopabVD  37961
  Copyright terms: Public domain W3C validator