Theorem eleq2d 2299

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 2293	. 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 1395   e. wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eleq12d  2300  eleqtrd  2308  neleqtrd  2327  neleqtrrd  2328  abeq2d  2342  nfceqdf  2371  drnfc1  2389  drnfc2  2390  sbcbid  3086  cbvcsbw  3128  cbvcsb  3129  sbcel1g  3143  csbeq2d  3149  csbie2g  3175  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  opeq1  3857  opeq2  3858  cbviun  4002  cbviin  4003  iinxsng  4039  iinxprg  4040  iunxsng  4041  iunxsngf  4043  cbvdisj  4069  disjnim  4073  disjiun  4078  mpteq12f  4164  axpweq  4255  rabxfrd  4560  onsucelsucexmid  4622  ordsucunielexmid  4623  0elsucexmid  4657  0nelelxp  4748  opeliunxp  4774  opeliunxp2  4862  iunxpf  4870  elrelimasn  5094  elimasng  5096  xpimasn  5177  ressn  5269  funfni  5423  fnbr  5425  fun11iun  5595  fvelrnb  5683  foelcdmi  5688  fvun1  5702  fvco2  5705  elfvmptrab1  5731  elfvmptrab  5732  elpreima  5756  dff3im  5782  resflem  5801  fmptco  5803  funfvima3  5877  foima2  5881  eluniimadm  5895  dff13  5898  f1eqcocnv  5921  isoini  5948  riotaeqdv  5961  mpoeq123dva  6071  cbvmpox  6088  ovelrn  6160  elovmpod  6209  elovmpo  6210  elovmporab  6211  elovmporab1w  6212  fmpox  6352  disjxp1  6388  opeliunxp2f  6390  mpoxopn0yelv  6391  mpoxopovel  6393  rbropapd  6394  rntpos  6409  smoel  6452  smoiso  6454  smoel2  6455  tfrlem9  6471  tfrlemisucaccv  6477  tfrlemiubacc  6482  tfrlemi14d  6485  tfri2d  6488  tfr1onlemubacc  6498  tfr1onlemres  6501  tfrcllemubacc  6511  tfrcllemres  6514  rdgon  6538  freceq1  6544  freceq2  6545  frec0g  6549  frecabcl  6551  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecsuc  6559  nnsucelsuc  6645  nnsucuniel  6649  nnmordi  6670  ereldm  6733  iinerm  6762  elmapg  6816  elpmg  6819  elixpsn  6890  ixpsnf1o  6891  pw2f1odclem  7003  phplem4  7024  phplem3g  7025  phplem4on  7037  exmidpw  7081  fiintim  7104  fidcenumlemrks  7131  fidcenumlemrk  7132  elfi  7149  ordiso2  7213  ctssdccl  7289  nnnninfeq  7306  cc2lem  7463  cc2  7464  cc3  7465  archnqq  7615  ltdfpr  7704  genpelxp  7709  genpelvl  7710  genpelvu  7711  addcanprleml  7812  addcanprlemu  7813  cauappcvgprlem1  7857  suplocexprlemell  7911  suplocexprlemmu  7916  suplocexprlemru  7917  suplocexprlemdisj  7918  suplocexprlemloc  7919  suplocexprlemub  7921  suplocexprlemlub  7922  cnm  8030  eluz1  9737  elixx1  10105  elioo2  10129  elfz1  10221  elfzp1  10280  fzpr  10285  fzsuc2  10287  fzrev3  10295  elfzp12  10307  fzm1  10308  fzoval  10356  elfzo  10357  fzodcel  10361  elfzom1b  10447  fzosplitsni  10453  nninfdcex  10469  zmodidfzo  10587  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  seqf1og  10755  bcval  10983  bcpasc  11000  fundm2domnop0  11080  wrdmap  11116  elovmpowrd  11126  ccatfvalfi  11140  elfzelfzccat  11148  ccatlid  11154  ccatass  11156  ccatrn  11157  ccatalpha  11161  swrdfv2  11211  ccatswrd  11218  swrdccat2  11219  pfxfv  11232  pfxeq  11244  ccatpfx  11249  swrdswrd  11253  swrdpfx  11255  pfxpfx  11256  cats1un  11269  swrdccatfn  11272  swrdccatin1  11273  pfxccatin12lem4  11274  pfxccatin12lem1  11276  swrdccatin2  11277  pfxccatin12lem2c  11278  pfxccatin12lem2  11279  swrdccat3blem  11287  swrdccatin1d  11291  swrdccatin2d  11292  pfxccatin12d  11293  shftfn  11351  shftval  11352  seq3shft  11365  iser3shft  11873  sumeq1  11882  summodclem3  11907  summodclem2a  11908  isumss  11918  fsumsplit  11934  sumsplitdc  11959  fsum2dlemstep  11961  fisumcom2  11965  fsumparts  11997  explecnv  12032  fprodsplitdc  12123  fprodsplit  12124  fprod2dlemstep  12149  fprodcom2fi  12153  eftlub  12217  divalgmod  12454  bitsval  12470  bitsp1e  12479  bitsp1o  12480  algfx  12590  eucalgcvga  12596  reumodprminv  12792  nnnn0modprm0  12794  ennnfonelemex  13001  ennnfonelemhom  13002  ennnfonelemf1  13005  ennnfonelemrn  13006  ctinfomlemom  13014  ctinfom  13015  ctiunctlemudc  13024  ctiunctlemf  13025  elrest  13295  ptex  13313  prdsbasmpt  13329  prdsbasmpt2  13337  pwselbasb  13342  imasaddfnlemg  13363  divsfval  13377  xpscf  13396  grpidvalg  13422  grpidpropdg  13423  grpidd  13432  issgrpd  13461  sgrppropd  13462  ismndd  13486  mndpropd  13489  imasmnd2  13501  imasmnd  13502  ismhm  13510  issubm  13521  imasgrp2  13663  imasgrp  13664  issubg  13726  subginv  13734  isnsg  13755  eqg0el  13782  quselbasg  13783  isghm  13796  resghm2b  13815  conjnmzb  13833  conjnsg  13834  ghmpropd  13836  imasabl  13889  isrngd  13932  rngpropd  13934  imasrng  13935  qusrng  13937  dfur2g  13941  srgidmlem  13957  issrgid  13960  ringcl  13992  isringid  14004  isringd  14020  imasring  14043  oppr0g  14060  oppr1g  14061  dvdsrvald  14073  isunitd  14086  unitinvcl  14103  unitinvinv  14104  unitlinv  14106  unitrinv  14107  unitnegcl  14110  dvdsrpropdg  14127  isrhm  14138  isrim0  14141  rhmmul  14144  islring  14172  issubrng  14179  opprsubrngg  14191  issubrg  14201  resrhm2b  14229  rhmpropd  14234  rrgval  14242  aprval  14262  aprap  14266  islmod  14271  lmodprop2d  14328  islssm  14337  islssmg  14338  islssmd  14339  lssats2  14394  ellspsn  14397  ixpsnbasval  14446  islidlm  14459  isridlrng  14462  rspssp  14474  rnglidlmmgm  14476  2idlval  14482  isridl  14484  2idlelb  14485  quscrng  14513  rspsn  14514  zrhval  14597  zrhrhmb  14602  znf1o  14631  psrgrp  14665  mplelbascoe  14672  istopon  14703  eltg  14742  eltg2  14743  eltop  14759  eltop2  14760  eltop3  14761  iscld  14793  neiss2  14832  isnei  14834  lmfval  14883  cnfval  14884  iscn  14887  iscnp  14889  tgcn  14898  tgcnp  14899  lmbrf  14905  cnptopresti  14928  txbas  14948  eltx  14949  txdis  14967  txdis1cn  14968  hmeofvalg  14993  ishmeo  14994  ispsmet  15013  ismet  15034  isxmet  15035  elblps  15080  elbl  15081  elmopn  15136  neibl  15181  metrest  15196  txmetcnp  15208  txmetcn  15209  metcnpd  15210  elcncf  15263  ellimc3apf  15350  limcmpted  15353  cnlimcim  15361  cnlimc  15362  eldvap  15372  dvidsslem  15383  dviaddf  15395  dvimulf  15396  elply  15424  ply1termlem  15432  lgseisenlem3  15767  edgiedgbg  15881  edgupgren  15955  upgredg  15958  uhgr2edg  16020  umgr2edg1  16023  usgredg2vlem1  16036  usgredg2vlem2  16037  ushgredgedg  16040  ushgredgedgloop  16042  vtxdgfval  16048  vtxedgfi  16049  vtxdgop  16052  vtxdg0v  16054  vtxdeqd  16056  vtxdfifiun  16057  wksfval  16068  iswlk  16069  wlkm  16085  uspgr2wlkeq  16111  wlkreslem  16122  wlkres  16123  istrl  16129  clwwlkg  16136  isclwwlk  16137  clwwlkccatlem  16143  isclwwlkng  16149  clwwlkn0  16151  clwwlknnn  16155  clwwlkext2edg  16164  bj-sels  16360  2omap  16446  pw1map  16448  nninfall  16463  nninfsellemeq  16468