Theorem eleq2d 2263

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 2257	. 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 2164

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 2175

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

This theorem is referenced by:  eleq12d  2264  eleqtrd  2272  neleqtrd  2291  neleqtrrd  2292  abeq2d  2306  nfceqdf  2335  drnfc1  2353  drnfc2  2354  sbcbid  3044  cbvcsbw  3085  cbvcsb  3086  sbcel1g  3100  csbeq2d  3106  csbie2g  3132  cbvralcsf  3144  cbvrexcsf  3145  cbvreucsf  3146  cbvrabcsf  3147  opeq1  3805  opeq2  3806  cbviun  3950  cbviin  3951  iinxsng  3987  iinxprg  3988  iunxsng  3989  iunxsngf  3991  cbvdisj  4017  disjnim  4021  disjiun  4025  mpteq12f  4110  axpweq  4201  rabxfrd  4501  onsucelsucexmid  4563  ordsucunielexmid  4564  0elsucexmid  4598  0nelelxp  4689  opeliunxp  4715  opeliunxp2  4803  iunxpf  4811  elrelimasn  5032  elimasng  5034  xpimasn  5115  ressn  5207  funfni  5355  fnbr  5357  fun11iun  5522  fvelrnb  5605  foelcdmi  5610  fvun1  5624  fvco2  5627  elfvmptrab1  5653  elfvmptrab  5654  elpreima  5678  dff3im  5704  resflem  5723  fmptco  5725  funfvima3  5793  foima2  5795  eluniimadm  5809  dff13  5812  f1eqcocnv  5835  isoini  5862  riotaeqdv  5875  mpoeq123dva  5980  cbvmpox  5997  ovelrn  6069  elovmpod  6118  elovmpo  6119  elovmporab  6120  elovmporab1w  6121  fmpox  6255  disjxp1  6291  opeliunxp2f  6293  mpoxopn0yelv  6294  mpoxopovel  6296  rbropapd  6297  rntpos  6312  smoel  6355  smoiso  6357  smoel2  6358  tfrlem9  6374  tfrlemisucaccv  6380  tfrlemiubacc  6385  tfrlemi14d  6388  tfri2d  6391  tfr1onlemubacc  6401  tfr1onlemres  6404  tfrcllemubacc  6414  tfrcllemres  6417  rdgon  6441  freceq1  6447  freceq2  6448  frec0g  6452  frecabcl  6454  freccllem  6457  frecfcllem  6459  frecsuclem  6461  frecsuc  6462  nnsucelsuc  6546  nnsucuniel  6550  nnmordi  6571  ereldm  6634  iinerm  6663  elmapg  6717  elpmg  6720  elixpsn  6791  ixpsnf1o  6792  pw2f1odclem  6892  phplem4  6913  phplem3g  6914  phplem4on  6925  exmidpw  6966  fiintim  6987  fidcenumlemrks  7014  fidcenumlemrk  7015  elfi  7032  ordiso2  7096  ctssdccl  7172  nnnninfeq  7189  cc2lem  7328  cc2  7329  cc3  7330  archnqq  7479  ltdfpr  7568  genpelxp  7573  genpelvl  7574  genpelvu  7575  addcanprleml  7676  addcanprlemu  7677  cauappcvgprlem1  7721  suplocexprlemell  7775  suplocexprlemmu  7780  suplocexprlemru  7781  suplocexprlemdisj  7782  suplocexprlemloc  7783  suplocexprlemub  7785  suplocexprlemlub  7786  cnm  7894  eluz1  9599  elixx1  9966  elioo2  9990  elfz1  10082  elfzp1  10141  fzpr  10146  fzsuc2  10148  fzrev3  10156  elfzp12  10168  fzm1  10169  fzoval  10217  elfzo  10218  fzodcel  10222  elfzom1b  10299  fzosplitsni  10305  zmodidfzo  10427  frecuzrdgtcl  10486  frecuzrdgfunlem  10493  seqf1og  10595  bcval  10823  bcpasc  10840  wrdmap  10948  elovmpowrd  10958  shftfn  10971  shftval  10972  seq3shft  10985  iser3shft  11492  sumeq1  11501  summodclem3  11526  summodclem2a  11527  isumss  11537  fsumsplit  11553  sumsplitdc  11578  fsum2dlemstep  11580  fisumcom2  11584  fsumparts  11616  explecnv  11651  fprodsplitdc  11742  fprodsplit  11743  fprod2dlemstep  11768  fprodcom2fi  11772  eftlub  11836  divalgmod  12071  nninfdcex  12093  algfx  12193  eucalgcvga  12199  reumodprminv  12394  nnnn0modprm0  12396  ennnfonelemex  12574  ennnfonelemhom  12575  ennnfonelemf1  12578  ennnfonelemrn  12579  ctinfomlemom  12587  ctinfom  12588  ctiunctlemudc  12597  ctiunctlemf  12598  elrest  12860  ptex  12878  imasaddfnlemg  12900  divsfval  12914  xpscf  12933  grpidvalg  12959  grpidpropdg  12960  grpidd  12969  issgrpd  12998  sgrppropd  12999  ismndd  13021  mndpropd  13024  ismhm  13036  issubm  13047  imasgrp2  13183  imasgrp  13184  issubg  13246  subginv  13254  isnsg  13275  eqg0el  13302  quselbasg  13303  isghm  13316  resghm2b  13335  conjnmzb  13353  conjnsg  13354  ghmpropd  13356  imasabl  13409  isrngd  13452  rngpropd  13454  imasrng  13455  qusrng  13457  dfur2g  13461  srgidmlem  13477  issrgid  13480  ringcl  13512  isringid  13524  isringd  13540  imasring  13563  oppr0g  13580  oppr1g  13581  reldvdsrsrg  13591  dvdsrvald  13592  isunitd  13605  unitinvcl  13622  unitinvinv  13623  unitlinv  13625  unitrinv  13626  unitnegcl  13629  dvdsrpropdg  13646  isrhm  13657  isrim0  13660  rhmmul  13663  islring  13691  issubrng  13698  opprsubrngg  13710  issubrg  13720  resrhm2b  13748  rhmpropd  13753  rrgval  13761  aprval  13781  aprap  13785  islmod  13790  lmodprop2d  13847  islssm  13856  islssmg  13857  islssmd  13858  lssats2  13913  ellspsn  13916  ixpsnbasval  13965  islidlm  13978  isridlrng  13981  rspssp  13993  rnglidlmmgm  13995  2idlval  14001  isridl  14003  2idlelb  14004  quscrng  14032  rspsn  14033  zrhval  14116  zrhrhmb  14121  znf1o  14150  istopon  14192  eltg  14231  eltg2  14232  eltop  14248  eltop2  14249  eltop3  14250  iscld  14282  neiss2  14321  isnei  14323  lmfval  14371  cnfval  14373  iscn  14376  iscnp  14378  tgcn  14387  tgcnp  14388  lmbrf  14394  cnptopresti  14417  txbas  14437  eltx  14438  txdis  14456  txdis1cn  14457  hmeofvalg  14482  ishmeo  14483  ispsmet  14502  ismet  14523  isxmet  14524  elblps  14569  elbl  14570  elmopn  14625  neibl  14670  metrest  14685  txmetcnp  14697  txmetcn  14698  metcnpd  14699  elcncf  14752  ellimc3apf  14839  limcmpted  14842  cnlimcim  14850  cnlimc  14851  eldvap  14861  dvidsslem  14872  dviaddf  14884  dvimulf  14885  elply  14913  ply1termlem  14921  lgseisenlem3  15229  bj-sels  15476  nninfall  15569  nninfsellemeq  15574