Theorem eleq2d 2266

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

Step	Hyp	Ref	Expression
1		eleq1d.1	. 2 |- ( ph -> A = B )
2		eleq2 2260	. 2 |- ( A = B -> ( C e. A <-> C e. B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C e. A <-> C e. B ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1364   e. wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  eleq12d  2267  eleqtrd  2275  neleqtrd  2294  neleqtrrd  2295  abeq2d  2309  nfceqdf  2338  drnfc1  2356  drnfc2  2357  sbcbid  3047  cbvcsbw  3088  cbvcsb  3089  sbcel1g  3103  csbeq2d  3109  csbie2g  3135  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  opeq1  3808  opeq2  3809  cbviun  3953  cbviin  3954  iinxsng  3990  iinxprg  3991  iunxsng  3992  iunxsngf  3994  cbvdisj  4020  disjnim  4024  disjiun  4028  mpteq12f  4113  axpweq  4204  rabxfrd  4504  onsucelsucexmid  4566  ordsucunielexmid  4567  0elsucexmid  4601  0nelelxp  4692  opeliunxp  4718  opeliunxp2  4806  iunxpf  4814  elrelimasn  5035  elimasng  5037  xpimasn  5118  ressn  5210  funfni  5358  fnbr  5360  fun11iun  5525  fvelrnb  5608  foelcdmi  5613  fvun1  5627  fvco2  5630  elfvmptrab1  5656  elfvmptrab  5657  elpreima  5681  dff3im  5707  resflem  5726  fmptco  5728  funfvima3  5796  foima2  5798  eluniimadm  5812  dff13  5815  f1eqcocnv  5838  isoini  5865  riotaeqdv  5878  mpoeq123dva  5983  cbvmpox  6000  ovelrn  6072  elovmpod  6121  elovmpo  6122  elovmporab  6123  elovmporab1w  6124  fmpox  6258  disjxp1  6294  opeliunxp2f  6296  mpoxopn0yelv  6297  mpoxopovel  6299  rbropapd  6300  rntpos  6315  smoel  6358  smoiso  6360  smoel2  6361  tfrlem9  6377  tfrlemisucaccv  6383  tfrlemiubacc  6388  tfrlemi14d  6391  tfri2d  6394  tfr1onlemubacc  6404  tfr1onlemres  6407  tfrcllemubacc  6417  tfrcllemres  6420  rdgon  6444  freceq1  6450  freceq2  6451  frec0g  6455  frecabcl  6457  freccllem  6460  frecfcllem  6462  frecsuclem  6464  frecsuc  6465  nnsucelsuc  6549  nnsucuniel  6553  nnmordi  6574  ereldm  6637  iinerm  6666  elmapg  6720  elpmg  6723  elixpsn  6794  ixpsnf1o  6795  pw2f1odclem  6895  phplem4  6916  phplem3g  6917  phplem4on  6928  exmidpw  6969  fiintim  6992  fidcenumlemrks  7019  fidcenumlemrk  7020  elfi  7037  ordiso2  7101  ctssdccl  7177  nnnninfeq  7194  cc2lem  7333  cc2  7334  cc3  7335  archnqq  7484  ltdfpr  7573  genpelxp  7578  genpelvl  7579  genpelvu  7580  addcanprleml  7681  addcanprlemu  7682  cauappcvgprlem1  7726  suplocexprlemell  7780  suplocexprlemmu  7785  suplocexprlemru  7786  suplocexprlemdisj  7787  suplocexprlemloc  7788  suplocexprlemub  7790  suplocexprlemlub  7791  cnm  7899  eluz1  9605  elixx1  9972  elioo2  9996  elfz1  10088  elfzp1  10147  fzpr  10152  fzsuc2  10154  fzrev3  10162  elfzp12  10174  fzm1  10175  fzoval  10223  elfzo  10224  fzodcel  10228  elfzom1b  10305  fzosplitsni  10311  nninfdcex  10327  zmodidfzo  10445  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  seqf1og  10613  bcval  10841  bcpasc  10858  wrdmap  10966  elovmpowrd  10976  shftfn  10989  shftval  10990  seq3shft  11003  iser3shft  11511  sumeq1  11520  summodclem3  11545  summodclem2a  11546  isumss  11556  fsumsplit  11572  sumsplitdc  11597  fsum2dlemstep  11599  fisumcom2  11603  fsumparts  11635  explecnv  11670  fprodsplitdc  11761  fprodsplit  11762  fprod2dlemstep  11787  fprodcom2fi  11791  eftlub  11855  divalgmod  12092  bitsval  12108  bitsp1e  12116  bitsp1o  12117  algfx  12220  eucalgcvga  12226  reumodprminv  12422  nnnn0modprm0  12424  ennnfonelemex  12631  ennnfonelemhom  12632  ennnfonelemf1  12635  ennnfonelemrn  12636  ctinfomlemom  12644  ctinfom  12645  ctiunctlemudc  12654  ctiunctlemf  12655  elrest  12917  ptex  12935  imasaddfnlemg  12957  divsfval  12971  xpscf  12990  grpidvalg  13016  grpidpropdg  13017  grpidd  13026  issgrpd  13055  sgrppropd  13056  ismndd  13078  mndpropd  13081  ismhm  13093  issubm  13104  imasgrp2  13240  imasgrp  13241  issubg  13303  subginv  13311  isnsg  13332  eqg0el  13359  quselbasg  13360  isghm  13373  resghm2b  13392  conjnmzb  13410  conjnsg  13411  ghmpropd  13413  imasabl  13466  isrngd  13509  rngpropd  13511  imasrng  13512  qusrng  13514  dfur2g  13518  srgidmlem  13534  issrgid  13537  ringcl  13569  isringid  13581  isringd  13597  imasring  13620  oppr0g  13637  oppr1g  13638  reldvdsrsrg  13648  dvdsrvald  13649  isunitd  13662  unitinvcl  13679  unitinvinv  13680  unitlinv  13682  unitrinv  13683  unitnegcl  13686  dvdsrpropdg  13703  isrhm  13714  isrim0  13717  rhmmul  13720  islring  13748  issubrng  13755  opprsubrngg  13767  issubrg  13777  resrhm2b  13805  rhmpropd  13810  rrgval  13818  aprval  13838  aprap  13842  islmod  13847  lmodprop2d  13904  islssm  13913  islssmg  13914  islssmd  13915  lssats2  13970  ellspsn  13973  ixpsnbasval  14022  islidlm  14035  isridlrng  14038  rspssp  14050  rnglidlmmgm  14052  2idlval  14058  isridl  14060  2idlelb  14061  quscrng  14089  rspsn  14090  zrhval  14173  zrhrhmb  14178  znf1o  14207  istopon  14249  eltg  14288  eltg2  14289  eltop  14305  eltop2  14306  eltop3  14307  iscld  14339  neiss2  14378  isnei  14380  lmfval  14428  cnfval  14430  iscn  14433  iscnp  14435  tgcn  14444  tgcnp  14445  lmbrf  14451  cnptopresti  14474  txbas  14494  eltx  14495  txdis  14513  txdis1cn  14514  hmeofvalg  14539  ishmeo  14540  ispsmet  14559  ismet  14580  isxmet  14581  elblps  14626  elbl  14627  elmopn  14682  neibl  14727  metrest  14742  txmetcnp  14754  txmetcn  14755  metcnpd  14756  elcncf  14809  ellimc3apf  14896  limcmpted  14899  cnlimcim  14907  cnlimc  14908  eldvap  14918  dvidsslem  14929  dviaddf  14941  dvimulf  14942  elply  14970  ply1termlem  14978  lgseisenlem3  15313  bj-sels  15560  nninfall  15653  nninfsellemeq  15658