Theorem eleq2d 2301

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 2295	. 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 1398   e. wcel 2202

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eleq12d  2302  eleqtrd  2310  neleqtrd  2329  neleqtrrd  2330  abeq2d  2344  nfceqdf  2374  drnfc1  2392  drnfc2  2393  sbcbid  3090  cbvcsbw  3132  cbvcsb  3133  sbcel1g  3147  csbeq2d  3153  csbie2g  3179  cbvralcsf  3191  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  rabsnif  3742  opeq1  3867  opeq2  3868  cbviun  4012  cbviin  4013  iinxsng  4049  iinxprg  4050  iunxsng  4051  iunxsngf  4053  cbvdisj  4079  disjnim  4083  disjiun  4088  mpteq12f  4174  axpweq  4267  rabxfrd  4572  onsucelsucexmid  4634  ordsucunielexmid  4635  0elsucexmid  4669  0nelelxp  4760  opeliunxp  4787  opeliunxp2  4876  iunxpf  4884  elrelimasn  5109  elimasng  5111  xpimasn  5192  ressn  5284  funfni  5439  fnbr  5441  fun11iun  5613  fvelrnb  5702  foelcdmi  5707  fvun1  5721  fvco2  5724  elfvmptrab1  5750  elfvmptrab  5751  elpreima  5775  dff3im  5800  resflem  5819  fmptco  5821  funfvima3  5898  foima2  5902  eluniimadm  5916  dff13  5919  f1eqcocnv  5942  isoini  5969  riotaeqdv  5982  mpoeq123dva  6092  cbvmpox  6109  ovelrn  6181  elovmpod  6230  elovmpo  6231  elovmporab  6232  elovmporab1w  6233  fmpox  6374  disjxp1  6410  elsuppfng  6420  elsuppfn  6421  suppfnss  6435  suppcofn  6444  opeliunxp2f  6447  mpoxopn0yelv  6448  mpoxopovel  6450  rbropapd  6451  rntpos  6466  smoel  6509  smoiso  6511  smoel2  6512  tfrlem9  6528  tfrlemisucaccv  6534  tfrlemiubacc  6539  tfrlemi14d  6542  tfri2d  6545  tfr1onlemubacc  6555  tfr1onlemres  6558  tfrcllemubacc  6568  tfrcllemres  6571  rdgon  6595  freceq1  6601  freceq2  6602  frec0g  6606  frecabcl  6608  freccllem  6611  frecfcllem  6613  frecsuclem  6615  frecsuc  6616  nnsucelsuc  6702  nnsucuniel  6706  nnmordi  6727  ereldm  6790  iinerm  6819  elmapg  6873  elpmg  6876  elixpsn  6947  ixpsnf1o  6948  pw2f1odclem  7063  phplem4  7084  phplem3g  7085  phplem4on  7097  exmidpw  7143  fiintim  7166  fidcenumlemrks  7195  fidcenumlemrk  7196  elfi  7230  ordiso2  7294  ctssdccl  7370  nnnninfeq  7387  cc2lem  7545  cc2  7546  cc3  7547  archnqq  7697  ltdfpr  7786  genpelxp  7791  genpelvl  7792  genpelvu  7793  addcanprleml  7894  addcanprlemu  7895  cauappcvgprlem1  7939  suplocexprlemell  7993  suplocexprlemmu  7998  suplocexprlemru  7999  suplocexprlemdisj  8000  suplocexprlemloc  8001  suplocexprlemub  8003  suplocexprlemlub  8004  cnm  8112  eluz1  9820  elixx1  10193  elioo2  10217  elfz1  10310  elfzp1  10369  fzpr  10374  fzsuc2  10376  fzrev3  10384  elfzp12  10396  fzm1  10397  fzoval  10445  elfzo  10446  fzodcel  10450  elfzom1b  10537  fzosplitsni  10544  nninfdcex  10560  zmodidfzo  10678  frecuzrdgtcl  10737  frecuzrdgfunlem  10744  seqf1og  10846  bcval  11074  bcpasc  11091  fundm2domnop0  11175  wrdmap  11211  elovmpowrd  11221  ccatfvalfi  11235  elfzelfzccat  11243  ccatlid  11249  ccatass  11251  ccatrn  11252  ccatalpha  11256  swrdfv2  11310  ccatswrd  11317  swrdccat2  11318  pfxfv  11331  pfxeq  11343  ccatpfx  11348  swrdswrd  11352  swrdpfx  11354  pfxpfx  11355  cats1un  11368  swrdccatfn  11371  swrdccatin1  11372  pfxccatin12lem4  11373  pfxccatin12lem1  11375  swrdccatin2  11376  pfxccatin12lem2c  11377  pfxccatin12lem2  11378  swrdccat3blem  11386  swrdccatin1d  11390  swrdccatin2d  11391  pfxccatin12d  11392  shftfn  11464  shftval  11465  seq3shft  11478  iser3shft  11986  sumeq1  11995  summodclem3  12021  summodclem2a  12022  isumss  12032  fsumsplit  12048  sumsplitdc  12073  fsum2dlemstep  12075  fisumcom2  12079  fsumparts  12111  explecnv  12146  fprodsplitdc  12237  fprodsplit  12238  fprod2dlemstep  12263  fprodcom2fi  12267  eftlub  12331  divalgmod  12568  bitsval  12584  bitsp1e  12593  bitsp1o  12594  algfx  12704  eucalgcvga  12710  reumodprminv  12906  nnnn0modprm0  12908  ennnfonelemex  13115  ennnfonelemhom  13116  ennnfonelemf1  13119  ennnfonelemrn  13120  ctinfomlemom  13128  ctinfom  13129  ctiunctlemudc  13138  ctiunctlemf  13139  elrest  13409  ptex  13427  prdsbasmpt  13443  prdsbasmpt2  13451  pwselbasb  13456  imasaddfnlemg  13477  divsfval  13491  xpscf  13510  grpidvalg  13536  grpidpropdg  13537  grpidd  13546  issgrpd  13575  sgrppropd  13576  ismndd  13600  mndpropd  13603  imasmnd2  13615  imasmnd  13616  ismhm  13624  issubm  13635  imasgrp2  13777  imasgrp  13778  issubg  13840  subginv  13848  isnsg  13869  eqg0el  13896  quselbasg  13897  isghm  13910  resghm2b  13929  conjnmzb  13947  conjnsg  13948  ghmpropd  13950  imasabl  14003  gsumsplit0  14013  isrngd  14047  rngpropd  14049  imasrng  14050  qusrng  14052  dfur2g  14056  srgidmlem  14072  issrgid  14075  ringcl  14107  isringid  14119  isringd  14135  imasring  14158  oppr0g  14175  oppr1g  14176  dvdsrvald  14188  isunitd  14201  unitinvcl  14218  unitinvinv  14219  unitlinv  14221  unitrinv  14222  unitnegcl  14225  dvdsrpropdg  14242  isrhm  14253  isrim0  14256  rhmmul  14259  islring  14287  issubrng  14294  opprsubrngg  14306  issubrg  14316  resrhm2b  14344  rhmpropd  14349  rrgval  14357  aprval  14378  aprap  14382  islmod  14387  lmodprop2d  14444  islssm  14453  islssmg  14454  islssmd  14455  lssats2  14510  ellspsn  14513  ixpsnbasval  14562  islidlm  14575  isridlrng  14578  rspssp  14590  rnglidlmmgm  14592  2idlval  14598  isridl  14600  2idlelb  14601  quscrng  14629  rspsn  14630  zrhval  14713  zrhrhmb  14718  znf1o  14747  psrgrp  14786  mplelbascoe  14793  istopon  14824  eltg  14863  eltg2  14864  eltop  14880  eltop2  14881  eltop3  14882  iscld  14914  neiss2  14953  isnei  14955  lmfval  15004  cnfval  15005  iscn  15008  iscnp  15010  tgcn  15019  tgcnp  15020  lmbrf  15026  cnptopresti  15049  txbas  15069  eltx  15070  txdis  15088  txdis1cn  15089  hmeofvalg  15114  ishmeo  15115  ispsmet  15134  ismet  15155  isxmet  15156  elblps  15201  elbl  15202  elmopn  15257  neibl  15302  metrest  15317  txmetcnp  15329  txmetcn  15330  metcnpd  15331  elcncf  15384  ellimc3apf  15471  limcmpted  15474  cnlimcim  15482  cnlimc  15483  eldvap  15493  dvidsslem  15504  dviaddf  15516  dvimulf  15517  elply  15545  ply1termlem  15553  lgseisenlem3  15891  edgval  16001  edgiedgbg  16006  edgupgren  16082  upgredg  16085  uhgr2edg  16147  umgr2edg1  16150  usgredg2vlem1  16163  usgredg2vlem2  16164  ushgredgedg  16167  ushgredgedgloop  16169  subgruhgredgdm  16211  uhgrspansubgrlem  16217  vtxdgfval  16229  vtxedgfi  16230  vtxdgop  16233  vtxdg0v  16235  vtxdeqd  16237  vtxdfifiun  16238  1loopgrvd0fi  16247  1hevtxdg0fi  16248  1hevtxdg1en  16249  wksfval  16263  iswlk  16264  wlkm  16280  uspgr2wlkeq  16306  wlkreslem  16319  wlkres  16320  istrl  16326  clwwlkg  16334  isclwwlk  16335  clwwlkccatlem  16341  isclwwlkng  16347  clwwlkn0  16349  clwwlknnn  16353  clwwlkext2edg  16363  clwwlknonmpo  16369  clwwlknon  16370  clwwlk0on0  16372  iseupth  16388  eupth2lem3lem3fi  16411  eupth2lem3lem6fi  16412  eupth2lem3lem4fi  16414  eupth2lembfi  16418  bj-sels  16630  2omap  16715  pw1map  16717  nninfall  16735  nninfsellemeq  16740