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

Theorem opeq1 4784
 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 2903 . . . 4 (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
21anbi1d 632 . . 3 (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3 sneq 4558 . . . 4 (𝐴 = 𝐵 → {𝐴} = {𝐵})
4 preq1 4650 . . . 4 (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
53, 4preq12d 4658 . . 3 (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
62, 5ifbieq1d 4471 . 2 (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7 dfopif 4781 . 2 𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8 dfopif 4781 . 2 𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
96, 7, 83eqtr4g 2884 1 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2115  Vcvv 3479  ∅c0 4274  ifcif 4448  {csn 4548  {cpr 4550  ⟨cop 4554 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-rab 3141  df-v 3481  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-sn 4549  df-pr 4551  df-op 4555 This theorem is referenced by:  opeq12  4786  opeq1i  4787  opeq1d  4790  oteq1  4793  breq1  5050  cbvopab1  5120  cbvopab1g  5121  cbvopab1s  5123  opthg  5350  eqvinop  5359  sbcop1  5360  opelopabsb  5398  opelxp  5572  elvvv  5608  opabid2  5681  opeliunxp2  5690  elsnres  5873  elimasng  5936  dmsnopg  6051  reuop  6125  funopg  6370  f1osng  6636  f1oprswap  6639  dmfco  6738  fvelrn  6825  fsng  6880  funsneqopb  6895  fprg  6898  fvrnressn  6904  funfvima3  6980  oveq1  7145  oprabidw  7169  oprabid  7170  dfoprab2  7194  cbvoprab1  7223  elxp4  7610  elxp5  7611  opabex3d  7649  opabex3rd  7650  opabex3  7651  op1stg  7684  op2ndg  7685  el2xptp  7718  dfoprab4f  7737  frxp  7803  opeliunxp2f  7859  tfrlem11  8007  omeu  8194  oeeui  8211  elixpsn  8484  fundmen  8566  xpsnen  8584  xpassen  8594  xpf1o  8663  unxpdomlem1  8706  djur  9332  dfac5lem1  9534  dfac5lem4  9537  axdc4lem  9862  nqereu  10336  mulcanenq  10367  archnq  10387  prlem934  10440  supsrlem  10518  supsr  10519  swrdccatin1  14076  swrdccat3blem  14090  fsum2dlem  15114  fprod2dlem  15323  vdwlem10  16313  imasaddfnlem  16790  catideu  16935  iscatd2  16941  catlid  16943  catpropd  16968  symg2bas  18510  efgmval  18827  efgi  18834  vrgpval  18882  gsumcom2  19084  txkgen  22246  cnmpt21  22265  xkoinjcn  22281  txconn  22283  pt1hmeo  22400  cnextfvval  22659  qustgplem  22715  dvbsss  24494  axlowdim2  26743  axlowdim  26744  axcontlem10  26756  axcontlem12  26758  isnvlem  28382  br8d  30358  cnvoprabOLD  30453  prsrn  31176  esum2dlem  31369  eulerpartlemgvv  31652  satf0op  32642  satffunlem1lem1  32667  satffunlem2lem1  32669  sategoelfvb  32684  br8  33010  br6  33011  br4  33012  eldm3  33015  dfdm5  33034  elfuns  33394  brimg  33416  brapply  33417  brsuccf  33420  brrestrict  33428  dfrdg4  33430  cgrdegen  33483  brofs  33484  cgrextend  33487  brifs  33522  ifscgr  33523  brcgr3  33525  brcolinear2  33537  colineardim1  33540  brfs  33558  idinside  33563  btwnconn1lem7  33572  btwnconn1lem11  33576  btwnconn1lem12  33577  brsegle  33587  outsideofeu  33610  fvray  33620  linedegen  33622  fvline  33623  bj-inftyexpiinv  34526  bj-inftyexpidisj  34528  finxpeq2  34706  finxpreclem6  34715  finxpsuclem  34716  curfv  34937  isdivrngo  35288  drngoi  35289  dicelval3  38376  dihjatcclem4  38617  dropab1  40987  relopabVD  41443  funressndmafv2rn  43621  dfatdmfcoafv2  43652  ichnreuop  43831  ichreuopeq  43832  reuopreuprim  43885
 Copyright terms: Public domain W3C validator