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

Theorem eleq2d 2259
Description: Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.)
Hypothesis
Ref Expression
eleq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
eleq2d  |-  ( ph  ->  ( C  e.  A  <->  C  e.  B ) )

Proof of Theorem eleq2d
StepHypRef Expression
1 eleq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 eleq2 2253 . 2  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
31, 2syl 14 1  |-  ( ph  ->  ( C  e.  A  <->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105    = wceq 1364    e. wcel 2160
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2171
This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-clel 2185
This theorem is referenced by:  eleq12d  2260  eleqtrd  2268  neleqtrd  2287  neleqtrrd  2288  abeq2d  2302  nfceqdf  2331  drnfc1  2349  drnfc2  2350  sbcbid  3035  cbvcsbw  3076  cbvcsb  3077  sbcel1g  3091  csbeq2d  3097  csbie2g  3122  cbvralcsf  3134  cbvrexcsf  3135  cbvreucsf  3136  cbvrabcsf  3137  opeq1  3793  opeq2  3794  cbviun  3938  cbviin  3939  iinxsng  3975  iinxprg  3976  iunxsng  3977  iunxsngf  3979  cbvdisj  4005  disjnim  4009  disjiun  4013  mpteq12f  4098  axpweq  4189  rabxfrd  4487  onsucelsucexmid  4547  ordsucunielexmid  4548  0elsucexmid  4582  0nelelxp  4673  opeliunxp  4699  opeliunxp2  4785  iunxpf  4793  elrelimasn  5012  elimasng  5014  xpimasn  5095  ressn  5187  funfni  5335  fnbr  5337  fun11iun  5501  fvelrnb  5584  foelcdmi  5589  fvun1  5603  fvco2  5606  elfvmptrab1  5631  elfvmptrab  5632  elpreima  5656  dff3im  5682  resflem  5701  fmptco  5703  funfvima3  5771  foima2  5773  eluniimadm  5787  dff13  5790  f1eqcocnv  5813  isoini  5840  riotaeqdv  5853  mpoeq123dva  5957  cbvmpox  5974  ovelrn  6045  elovmpod  6094  elovmpo  6095  fmpox  6225  disjxp1  6261  opeliunxp2f  6263  mpoxopn0yelv  6264  mpoxopovel  6266  rbropapd  6267  rntpos  6282  smoel  6325  smoiso  6327  smoel2  6328  tfrlem9  6344  tfrlemisucaccv  6350  tfrlemiubacc  6355  tfrlemi14d  6358  tfri2d  6361  tfr1onlemubacc  6371  tfr1onlemres  6374  tfrcllemubacc  6384  tfrcllemres  6387  rdgon  6411  freceq1  6417  freceq2  6418  frec0g  6422  frecabcl  6424  freccllem  6427  frecfcllem  6429  frecsuclem  6431  frecsuc  6432  nnsucelsuc  6516  nnsucuniel  6520  nnmordi  6541  ereldm  6604  iinerm  6633  elmapg  6687  elpmg  6690  elixpsn  6761  ixpsnf1o  6762  pw2f1odclem  6862  phplem4  6883  phplem3g  6884  phplem4on  6895  exmidpw  6936  fiintim  6957  fidcenumlemrks  6982  fidcenumlemrk  6983  elfi  7000  ordiso2  7064  ctssdccl  7140  nnnninfeq  7156  cc2lem  7295  cc2  7296  cc3  7297  archnqq  7446  ltdfpr  7535  genpelxp  7540  genpelvl  7541  genpelvu  7542  addcanprleml  7643  addcanprlemu  7644  cauappcvgprlem1  7688  suplocexprlemell  7742  suplocexprlemmu  7747  suplocexprlemru  7748  suplocexprlemdisj  7749  suplocexprlemloc  7750  suplocexprlemub  7752  suplocexprlemlub  7753  cnm  7861  eluz1  9562  elixx1  9927  elioo2  9951  elfz1  10043  elfzp1  10102  fzpr  10107  fzsuc2  10109  fzrev3  10117  elfzp12  10129  fzm1  10130  fzoval  10178  elfzo  10179  fzodcel  10182  elfzom1b  10259  fzosplitsni  10265  zmodidfzo  10384  frecuzrdgtcl  10443  frecuzrdgfunlem  10450  bcval  10761  bcpasc  10778  shftfn  10865  shftval  10866  seq3shft  10879  iser3shft  11386  sumeq1  11395  summodclem3  11420  summodclem2a  11421  isumss  11431  fsumsplit  11447  sumsplitdc  11472  fsum2dlemstep  11474  fisumcom2  11478  fsumparts  11510  explecnv  11545  fprodsplitdc  11636  fprodsplit  11637  fprod2dlemstep  11662  fprodcom2fi  11666  eftlub  11730  divalgmod  11964  nninfdcex  11986  algfx  12084  eucalgcvga  12090  reumodprminv  12285  nnnn0modprm0  12287  ennnfonelemex  12465  ennnfonelemhom  12466  ennnfonelemf1  12469  ennnfonelemrn  12470  ctinfomlemom  12478  ctinfom  12479  ctiunctlemudc  12488  ctiunctlemf  12489  elrest  12751  ptex  12769  imasaddfnlemg  12791  xpscf  12823  grpidvalg  12849  grpidpropdg  12850  grpidd  12859  issgrpd  12875  sgrppropd  12876  ismndd  12898  mndpropd  12901  ismhm  12913  issubm  12924  imasgrp2  13052  imasgrp  13053  issubg  13112  subginv  13120  isnsg  13141  eqg0el  13168  quselbasg  13169  isghm  13182  resghm2b  13201  conjnmzb  13219  conjnsg  13220  ghmpropd  13222  imasabl  13273  isrngd  13307  rngpropd  13309  imasrng  13310  qusrng  13312  dfur2g  13316  srgidmlem  13332  issrgid  13335  ringcl  13367  isringid  13379  isringd  13395  imasring  13414  oppr0g  13431  oppr1g  13432  reldvdsrsrg  13442  dvdsrvald  13443  isunitd  13456  unitinvcl  13473  unitinvinv  13474  unitlinv  13476  unitrinv  13477  unitnegcl  13480  dvdsrpropdg  13497  isrhm  13508  isrim0  13511  rhmmul  13514  islring  13539  issubrng  13546  opprsubrngg  13558  issubrg  13568  aprval  13598  aprap  13602  islmod  13607  lmodprop2d  13664  islssm  13673  islssmg  13674  islssmd  13675  lssats2  13730  lspsnel  13733  ixpsnbasval  13782  islidlm  13795  isridlrng  13798  rspssp  13810  rnglidlmmgm  13812  isridl  13819  2idlelb  13820  quscrng  13847  zrhrhmb  13919  istopon  13970  eltg  14009  eltg2  14010  eltop  14026  eltop2  14027  eltop3  14028  iscld  14060  neiss2  14099  isnei  14101  lmfval  14149  cnfval  14151  iscn  14154  iscnp  14156  tgcn  14165  tgcnp  14166  lmbrf  14172  cnptopresti  14195  txbas  14215  eltx  14216  txdis  14234  txdis1cn  14235  hmeofvalg  14260  ishmeo  14261  ispsmet  14280  ismet  14301  isxmet  14302  elblps  14347  elbl  14348  elmopn  14403  neibl  14448  metrest  14463  txmetcnp  14475  txmetcn  14476  metcnpd  14477  elcncf  14517  ellimc3apf  14586  limcmpted  14589  cnlimcim  14597  cnlimc  14598  eldvap  14608  dviaddf  14626  dvimulf  14627  bj-sels  15124  nninfall  15217  nninfsellemeq  15222
  Copyright terms: Public domain W3C validator