ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eleq2d GIF version

Theorem eleq2d 2209
Description: Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.)
Hypothesis
Ref Expression
eleq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
eleq2d (𝜑 → (𝐶𝐴𝐶𝐵))

Proof of Theorem eleq2d
StepHypRef Expression
1 eleq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 eleq2 2203 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2syl 14 1 (𝜑 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1331  wcel 1480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135
This theorem is referenced by:  eleq12d  2210  eleqtrd  2218  neleqtrd  2237  neleqtrrd  2238  abeq2d  2252  nfceqdf  2280  drnfc1  2298  drnfc2  2299  sbcbid  2966  cbvcsbw  3007  cbvcsb  3008  sbcel1g  3021  csbeq2d  3027  csbie2g  3050  cbvralcsf  3062  cbvrexcsf  3063  cbvreucsf  3064  cbvrabcsf  3065  opeq1  3705  opeq2  3706  cbviun  3850  cbviin  3851  iinxsng  3886  iinxprg  3887  iunxsng  3888  iunxsngf  3890  cbvdisj  3916  disjnim  3920  disjiun  3924  mpteq12f  4008  axpweq  4095  rabxfrd  4390  onsucelsucexmid  4445  ordsucunielexmid  4446  0elsucexmid  4480  0nelelxp  4568  opeliunxp  4594  opeliunxp2  4679  iunxpf  4687  elreimasng  4905  elimasng  4907  xpimasn  4987  ressn  5079  funfni  5223  fnbr  5225  fun11iun  5388  fvelrnb  5469  fvun1  5487  fvco2  5490  elfvmptrab1  5515  elfvmptrab  5516  elpreima  5539  dff3im  5565  resflem  5584  fmptco  5586  funfvima3  5651  foima2  5653  eluniimadm  5666  dff13  5669  f1eqcocnv  5692  isoini  5719  riotaeqdv  5731  mpoeq123dva  5832  cbvmpox  5849  ovelrn  5919  elovmpo  5971  fmpox  6098  disjxp1  6133  opeliunxp2f  6135  mpoxopn0yelv  6136  mpoxopovel  6138  rbropapd  6139  rntpos  6154  smoel  6197  smoiso  6199  smoel2  6200  tfrlem9  6216  tfrlemisucaccv  6222  tfrlemiubacc  6227  tfrlemi14d  6230  tfri2d  6233  tfr1onlemubacc  6243  tfr1onlemres  6246  tfrcllemubacc  6256  tfrcllemres  6259  rdgon  6283  freceq1  6289  freceq2  6290  frec0g  6294  frecabcl  6296  freccllem  6299  frecfcllem  6301  frecsuclem  6303  frecsuc  6304  nnsucelsuc  6387  nnsucuniel  6391  nnmordi  6412  ereldm  6472  iinerm  6501  elmapg  6555  elpmg  6558  elixpsn  6629  ixpsnf1o  6630  phplem4  6749  phplem3g  6750  phplem4on  6761  exmidpw  6802  fiintim  6817  fidcenumlemrks  6841  fidcenumlemrk  6842  elfi  6859  ordiso2  6920  ctssdccl  6996  cc2lem  7086  cc2  7087  cc3  7088  archnqq  7237  ltdfpr  7326  genpelxp  7331  genpelvl  7332  genpelvu  7333  addcanprleml  7434  addcanprlemu  7435  cauappcvgprlem1  7479  suplocexprlemell  7533  suplocexprlemmu  7538  suplocexprlemru  7539  suplocexprlemdisj  7540  suplocexprlemloc  7541  suplocexprlemub  7543  suplocexprlemlub  7544  cnm  7652  eluz1  9342  elixx1  9692  elioo2  9716  elfz1  9807  elfzp1  9864  fzpr  9869  fzsuc2  9871  fzrev3  9879  elfzp12  9891  fzm1  9892  fzoval  9937  elfzo  9938  fzodcel  9941  elfzom1b  10018  fzosplitsni  10024  zmodidfzo  10138  frecuzrdgtcl  10197  frecuzrdgfunlem  10204  bcval  10507  bcpasc  10524  shftfn  10608  shftval  10609  seq3shft  10622  iser3shft  11127  sumeq1  11136  summodclem3  11161  summodclem2a  11162  isumss  11172  fsumsplit  11188  sumsplitdc  11213  fsum2dlemstep  11215  fisumcom2  11219  fsumparts  11251  explecnv  11286  eftlub  11408  divalgmod  11635  algfx  11744  eucalgcvga  11750  ennnfonelemex  11938  ennnfonelemhom  11939  ennnfonelemf1  11942  ennnfonelemrn  11943  ctinfomlemom  11951  ctinfom  11952  ctiunctlemudc  11961  ctiunctlemf  11962  elrest  12141  istopon  12194  eltg  12235  eltg2  12236  eltop  12252  eltop2  12253  eltop3  12254  iscld  12286  neiss2  12325  isnei  12327  lmfval  12375  cnfval  12377  iscn  12380  iscnp  12382  tgcn  12391  tgcnp  12392  lmbrf  12398  cnptopresti  12421  txbas  12441  eltx  12442  txdis  12460  txdis1cn  12461  hmeofvalg  12486  ishmeo  12487  ispsmet  12506  ismet  12527  isxmet  12528  elblps  12573  elbl  12574  elmopn  12629  neibl  12674  metrest  12689  txmetcnp  12701  txmetcn  12702  metcnpd  12703  elcncf  12743  ellimc3apf  12812  limcmpted  12815  cnlimcim  12823  cnlimc  12824  eldvap  12834  dviaddf  12852  dvimulf  12853  bj-sels  13196  nninfalllemn  13288  nninfall  13290  nninfsellemeq  13296
  Copyright terms: Public domain W3C validator