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

Theorem opeq2 4434
Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
opeq2 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Proof of Theorem opeq2
StepHypRef Expression
1 eleq1 2718 . . . 4 (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
21anbi2d 740 . . 3 (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3 preq2 4301 . . . 4 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
43preq2d 4307 . . 3 (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
52, 4ifbieq1d 4142 . 2 (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6 dfopif 4430 . 2 𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7 dfopif 4430 . 2 𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
85, 6, 73eqtr4g 2710 1 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  wcel 2030  Vcvv 3231  c0 3948  ifcif 4119  {csn 4210  {cpr 4212  cop 4216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217
This theorem is referenced by:  opeq12  4435  opeq2i  4437  opeq2d  4440  oteq2  4443  oteq3  4444  breq2  4689  cbvopab2  4757  cbvopab2v  4760  opthg  4975  eqvinop  4984  opelopabsb  5014  dfid3  5054  opelxp  5180  relopabi  5278  opabid2  5284  elrn2g  5345  opeldmd  5359  opeldm  5360  elrn2  5397  opelresgOLD  5440  iss  5482  elimasng  5526  issref  5544  dmsnopg  5642  cnvsngOLD  5659  funopg  5960  f1osng  6215  f1oprswap  6218  tz6.12f  6250  fvn0ssdmfun  6390  fsn  6442  fsng  6444  funsneqopsn  6457  fprg  6462  fvsng  6488  oveq2  6698  cbvoprab2  6770  ovg  6841  elxp4  7152  elxp5  7153  opabex3d  7187  opabex3  7188  op1stg  7222  op2ndg  7223  op1steq  7254  dfoprab4f  7270  seqomlem2  7591  omeu  7710  oeeui  7727  ralxpmap  7949  elixpsn  7989  ixpsnf1o  7990  mapsnen  8076  xpsnen  8085  xpassen  8095  xpf1o  8163  unxpdomlem1  8205  axdc4lem  9315  nqereu  9789  mulcanenq  9820  elreal  9990  ax1rid  10020  fseq1p1m1  12452  swrdccatin1  13529  swrdccat3blem  13541  swrdccatid  13543  swrdccatin12d  13547  wrdlen2  13734  ruclem1  15004  imasaddfnlem  16235  imasvscafn  16244  catidex  16382  catpropd  16416  funcsetcestrclem1  16841  symg2bas  17864  psgnunilem5  17960  efgi  18178  gsumcom2  18420  mat1rhmval  20333  mat1ric  20341  txkgen  21503  cnmpt21  21522  xkoinjcn  21538  txconn  21540  xpstopnlem1  21660  qustgplem  21971  metustid  22406  axlowdim2  25885  axlowdim  25886  axcontlem2  25890  axcontlem3  25891  axcontlem4  25892  axcontlem9  25897  axcontlem10  25898  axcontlem11  25899  cusgrexg  26396  rgrusgrprc  26541  wwlksnextbi  26857  wwlksnextinj  26862  wwlksnextsur  26863  clwwlkfo  27013  clwlksfclwwlk  27049  2clwwlk2clwwlk  27338  isnvlem  27593  br8d  29548  prsdm  30088  eulerpartlemgvv  30566  reprsuc  30821  bnj941  30969  bnj944  31134  cvmlift2lem1  31410  cvmlift2lem12  31422  br8  31772  br6  31773  br4  31774  fprb  31795  br1steqgOLD  31798  br2ndeqgOLD  31799  dfrn5  31801  elima4  31803  pprodss4v  32116  brimg  32169  brapply  32170  brsuccf  32173  brrestrict  32181  dfrdg4  32183  cgrtriv  32234  brofs  32237  segconeu  32243  btwntriv2  32244  transportprops  32266  brifs  32275  ifscgr  32276  brcgr3  32278  cgrxfr  32287  brcolinear2  32290  colineardim1  32293  brfs  32311  idinside  32316  btwnconn1lem7  32325  btwnconn1lem11  32329  btwnconn1lem12  32330  btwnconn1lem14  32332  brsegle  32340  seglerflx  32344  seglemin  32345  segleantisym  32347  btwnsegle  32349  outsideofeu  32363  outsidele  32364  linedegen  32375  fvline  32376  finxpreclem6  33363  finxpsuclem  33364  curfv  33519  poimirlem4  33543  poimirlem26  33565  isdivrngo  33879  drngoi  33880  iss2  34252  dibelval3  36753  diblsmopel  36777  dihjatcclem4  37027  dfhe3  38386  dffrege115  38589  dropab2  38969  relopabVD  39451  projf1o  39700  mapsnend  39705  sge0xp  40964  hoidmv1le  41129  pfxval  41708
  Copyright terms: Public domain W3C validator