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 1397   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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  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  2373  drnfc1  2391  drnfc2  2392  sbcbid  3089  cbvcsbw  3131  cbvcsb  3132  sbcel1g  3146  csbeq2d  3152  csbie2g  3178  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  rabsnif  3738  opeq1  3862  opeq2  3863  cbviun  4007  cbviin  4008  iinxsng  4044  iinxprg  4045  iunxsng  4046  iunxsngf  4048  cbvdisj  4074  disjnim  4078  disjiun  4083  mpteq12f  4169  axpweq  4261  rabxfrd  4566  onsucelsucexmid  4628  ordsucunielexmid  4629  0elsucexmid  4663  0nelelxp  4754  opeliunxp  4781  opeliunxp2  4870  iunxpf  4878  elrelimasn  5102  elimasng  5104  xpimasn  5185  ressn  5277  funfni  5432  fnbr  5434  fun11iun  5604  fvelrnb  5693  foelcdmi  5698  fvun1  5712  fvco2  5715  elfvmptrab1  5741  elfvmptrab  5742  elpreima  5766  dff3im  5792  resflem  5811  fmptco  5813  funfvima3  5888  foima2  5892  eluniimadm  5906  dff13  5909  f1eqcocnv  5932  isoini  5959  riotaeqdv  5972  mpoeq123dva  6082  cbvmpox  6099  ovelrn  6171  elovmpod  6220  elovmpo  6221  elovmporab  6222  elovmporab1w  6223  fmpox  6365  disjxp1  6401  opeliunxp2f  6404  mpoxopn0yelv  6405  mpoxopovel  6407  rbropapd  6408  rntpos  6423  smoel  6466  smoiso  6468  smoel2  6469  tfrlem9  6485  tfrlemisucaccv  6491  tfrlemiubacc  6496  tfrlemi14d  6499  tfri2d  6502  tfr1onlemubacc  6512  tfr1onlemres  6515  tfrcllemubacc  6525  tfrcllemres  6528  rdgon  6552  freceq1  6558  freceq2  6559  frec0g  6563  frecabcl  6565  freccllem  6568  frecfcllem  6570  frecsuclem  6572  frecsuc  6573  nnsucelsuc  6659  nnsucuniel  6663  nnmordi  6684  ereldm  6747  iinerm  6776  elmapg  6830  elpmg  6833  elixpsn  6904  ixpsnf1o  6905  pw2f1odclem  7020  phplem4  7041  phplem3g  7042  phplem4on  7054  exmidpw  7100  fiintim  7123  fidcenumlemrks  7152  fidcenumlemrk  7153  elfi  7170  ordiso2  7234  ctssdccl  7310  nnnninfeq  7327  cc2lem  7485  cc2  7486  cc3  7487  archnqq  7637  ltdfpr  7726  genpelxp  7731  genpelvl  7732  genpelvu  7733  addcanprleml  7834  addcanprlemu  7835  cauappcvgprlem1  7879  suplocexprlemell  7933  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemub  7943  suplocexprlemlub  7944  cnm  8052  eluz1  9759  elixx1  10132  elioo2  10156  elfz1  10248  elfzp1  10307  fzpr  10312  fzsuc2  10314  fzrev3  10322  elfzp12  10334  fzm1  10335  fzoval  10383  elfzo  10384  fzodcel  10388  elfzom1b  10474  fzosplitsni  10481  nninfdcex  10497  zmodidfzo  10615  frecuzrdgtcl  10674  frecuzrdgfunlem  10681  seqf1og  10783  bcval  11011  bcpasc  11028  fundm2domnop0  11109  wrdmap  11145  elovmpowrd  11155  ccatfvalfi  11169  elfzelfzccat  11177  ccatlid  11183  ccatass  11185  ccatrn  11186  ccatalpha  11190  swrdfv2  11244  ccatswrd  11251  swrdccat2  11252  pfxfv  11265  pfxeq  11277  ccatpfx  11282  swrdswrd  11286  swrdpfx  11288  pfxpfx  11289  cats1un  11302  swrdccatfn  11305  swrdccatin1  11306  pfxccatin12lem4  11307  pfxccatin12lem1  11309  swrdccatin2  11310  pfxccatin12lem2c  11311  pfxccatin12lem2  11312  swrdccat3blem  11320  swrdccatin1d  11324  swrdccatin2d  11325  pfxccatin12d  11326  shftfn  11385  shftval  11386  seq3shft  11399  iser3shft  11907  sumeq1  11916  summodclem3  11942  summodclem2a  11943  isumss  11953  fsumsplit  11969  sumsplitdc  11994  fsum2dlemstep  11996  fisumcom2  12000  fsumparts  12032  explecnv  12067  fprodsplitdc  12158  fprodsplit  12159  fprod2dlemstep  12184  fprodcom2fi  12188  eftlub  12252  divalgmod  12489  bitsval  12505  bitsp1e  12514  bitsp1o  12515  algfx  12625  eucalgcvga  12631  reumodprminv  12827  nnnn0modprm0  12829  ennnfonelemex  13036  ennnfonelemhom  13037  ennnfonelemf1  13040  ennnfonelemrn  13041  ctinfomlemom  13049  ctinfom  13050  ctiunctlemudc  13059  ctiunctlemf  13060  elrest  13330  ptex  13348  prdsbasmpt  13364  prdsbasmpt2  13372  pwselbasb  13377  imasaddfnlemg  13398  divsfval  13412  xpscf  13431  grpidvalg  13457  grpidpropdg  13458  grpidd  13467  issgrpd  13496  sgrppropd  13497  ismndd  13521  mndpropd  13524  imasmnd2  13536  imasmnd  13537  ismhm  13545  issubm  13556  imasgrp2  13698  imasgrp  13699  issubg  13761  subginv  13769  isnsg  13790  eqg0el  13817  quselbasg  13818  isghm  13831  resghm2b  13850  conjnmzb  13868  conjnsg  13869  ghmpropd  13871  imasabl  13924  gsumsplit0  13934  isrngd  13968  rngpropd  13970  imasrng  13971  qusrng  13973  dfur2g  13977  srgidmlem  13993  issrgid  13996  ringcl  14028  isringid  14040  isringd  14056  imasring  14079  oppr0g  14096  oppr1g  14097  dvdsrvald  14109  isunitd  14122  unitinvcl  14139  unitinvinv  14140  unitlinv  14142  unitrinv  14143  unitnegcl  14146  dvdsrpropdg  14163  isrhm  14174  isrim0  14177  rhmmul  14180  islring  14208  issubrng  14215  opprsubrngg  14227  issubrg  14237  resrhm2b  14265  rhmpropd  14270  rrgval  14278  aprval  14298  aprap  14302  islmod  14307  lmodprop2d  14364  islssm  14373  islssmg  14374  islssmd  14375  lssats2  14430  ellspsn  14433  ixpsnbasval  14482  islidlm  14495  isridlrng  14498  rspssp  14510  rnglidlmmgm  14512  2idlval  14518  isridl  14520  2idlelb  14521  quscrng  14549  rspsn  14550  zrhval  14633  zrhrhmb  14638  znf1o  14667  psrgrp  14701  mplelbascoe  14708  istopon  14739  eltg  14778  eltg2  14779  eltop  14795  eltop2  14796  eltop3  14797  iscld  14829  neiss2  14868  isnei  14870  lmfval  14919  cnfval  14920  iscn  14923  iscnp  14925  tgcn  14934  tgcnp  14935  lmbrf  14941  cnptopresti  14964  txbas  14984  eltx  14985  txdis  15003  txdis1cn  15004  hmeofvalg  15029  ishmeo  15030  ispsmet  15049  ismet  15070  isxmet  15071  elblps  15116  elbl  15117  elmopn  15172  neibl  15217  metrest  15232  txmetcnp  15244  txmetcn  15245  metcnpd  15246  elcncf  15299  ellimc3apf  15386  limcmpted  15389  cnlimcim  15397  cnlimc  15398  eldvap  15408  dvidsslem  15419  dviaddf  15431  dvimulf  15432  elply  15460  ply1termlem  15468  lgseisenlem3  15803  edgval  15913  edgiedgbg  15918  edgupgren  15994  upgredg  15997  uhgr2edg  16059  umgr2edg1  16062  usgredg2vlem1  16075  usgredg2vlem2  16076  ushgredgedg  16079  ushgredgedgloop  16081  subgruhgredgdm  16123  uhgrspansubgrlem  16129  vtxdgfval  16141  vtxedgfi  16142  vtxdgop  16145  vtxdg0v  16147  vtxdeqd  16149  vtxdfifiun  16150  1loopgrvd0fi  16159  1hevtxdg0fi  16160  1hevtxdg1en  16161  wksfval  16175  iswlk  16176  wlkm  16192  uspgr2wlkeq  16218  wlkreslem  16231  wlkres  16232  istrl  16238  clwwlkg  16246  isclwwlk  16247  clwwlkccatlem  16253  isclwwlkng  16259  clwwlkn0  16261  clwwlknnn  16265  clwwlkext2edg  16275  clwwlknonmpo  16281  clwwlknon  16282  clwwlk0on0  16284  iseupth  16300  bj-sels  16512  2omap  16597  pw1map  16599  nninfall  16614  nninfsellemeq  16619