Theorem eleq2d 2308

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 2302	. 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 1402   e. wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is referenced by:  eleq12d  2309  eleqtrd  2317  neleqtrd  2336  neleqtrrd  2337  abeq2d  2351  eqabrd  2378  nfceqdf  2391  drnfc1  2409  drnfc2  2410  sbcbid  3109  cbvcsbw  3151  cbvcsb  3152  sbcel1g  3166  csbeq2d  3172  csbie2g  3198  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  rabsnif  3777  opeq1  3902  opeq2  3903  cbviun  4047  cbviin  4048  iinxsng  4084  iinxprg  4085  iunxsng  4086  iunxsngf  4088  cbvdisj  4114  disjnim  4118  disjiun  4123  mpteq12f  4209  axpweq  4306  rabxfrd  4613  onsucelsucexmid  4675  ordsucunielexmid  4676  0elsucexmid  4710  0nelelxp  4801  opeliunxp  4828  opeliunxp2  4918  iunxpf  4926  elrelimasn  5151  elimasng  5153  xpimasn  5234  ressn  5326  funfni  5481  fnbr  5483  fun11iun  5658  fvelrnb  5747  foelcdmi  5752  fvun1  5766  fvco2  5771  elfvmptrab1  5797  elfvmptrab  5798  elpreima  5822  dff3im  5847  resflem  5866  fmptco  5868  funfvima3  5945  foima2  5950  eluniimadm  5964  dff13  5967  f1eqcocnv  5990  isoini  6017  riotaeqdv  6032  mpoeq123dva  6142  cbvmpox  6159  ovelrn  6231  elovmpod  6280  elovmpo  6281  elovmporab  6282  elovmporab1w  6283  fmpox  6429  disjxp1  6465  elsuppfng  6475  elsuppfn  6476  suppfnss  6490  suppcofn  6499  opeliunxp2f  6502  mpoxopn0yelv  6503  mpoxopovel  6505  rbropapd  6506  rntpos  6521  smoel  6564  smoiso  6566  smoel2  6567  tfrlem9  6583  tfrlemisucaccv  6589  tfrlemiubacc  6594  tfrlemi14d  6597  tfri2d  6600  tfr1onlemubacc  6610  tfr1onlemres  6613  tfrcllemubacc  6623  tfrcllemres  6626  rdgon  6650  freceq1  6656  freceq2  6657  frec0g  6661  frecabcl  6663  freccllem  6666  frecfcllem  6668  frecsuclem  6670  frecsuc  6671  nnsucelsuc  6757  nnsucuniel  6761  nnmordi  6782  ereldm  6845  iinerm  6874  elmapg  6928  elpmg  6931  elixpsn  7010  ixpsnf1o  7011  pw2f1odclem  7127  phplem4  7149  phplem3g  7150  phplem4on  7162  exmidpw  7208  fiintim  7231  fidcenumlemrks  7263  fidcenumlemrk  7264  elfi  7298  2omap  7311  ordiso2  7368  ctssdccl  7444  nnnninfeq  7461  cc2lem  7625  cc2  7626  cc3  7627  archnqq  7777  ltdfpr  7866  genpelxp  7871  genpelvl  7872  genpelvu  7873  addcanprleml  7974  addcanprlemu  7975  cauappcvgprlem1  8019  suplocexprlemell  8073  suplocexprlemmu  8078  suplocexprlemru  8079  suplocexprlemdisj  8080  suplocexprlemloc  8081  suplocexprlemub  8083  suplocexprlemlub  8084  cnm  8192  eluz1  9907  elixx1  10281  elioo2  10305  elfz1  10398  elfzp1  10460  fzpr  10465  fzsuc2  10467  fzrev3  10475  elfzp12  10487  fzm1  10488  fzoval  10536  elfzo  10537  fzodcel  10541  elfzom1b  10628  fzosplitsni  10635  nninfdcex  10653  zmodidfzo  10771  frecuzrdgtcl  10830  frecuzrdgfunlem  10837  seqf1og  10939  bcval  11168  bcpasc  11185  hashf1lem1  11266  fundm2domnop0  11281  wrdmap  11317  elovmpowrd  11327  ccatfvalfi  11341  elfzelfzccat  11349  ccatlid  11355  ccatass  11357  ccatrn  11358  ccatalpha  11362  swrdfv2  11416  ccatswrd  11423  swrdccat2  11424  pfxfv  11437  pfxeq  11449  ccatpfx  11454  swrdswrd  11458  swrdpfx  11460  pfxpfx  11461  cats1un  11474  swrdccatfn  11477  swrdccatin1  11478  pfxccatin12lem4  11479  pfxccatin12lem1  11481  swrdccatin2  11482  pfxccatin12lem2c  11483  pfxccatin12lem2  11484  swrdccat3blem  11492  swrdccatin1d  11496  swrdccatin2d  11497  pfxccatin12d  11498  shftfn  11570  shftval  11571  seq3shft  11584  iser3shft  12093  sumeq1  12102  summodclem3  12128  summodclem2a  12129  isumss  12139  fsumsplit  12155  sumsplitdc  12180  fsum2dlemstep  12182  fisumcom2  12186  fsumparts  12218  explecnv  12253  fprodsplitdc  12344  fprodsplit  12345  fprod2dlemstep  12370  fprodcom2fi  12374  eftlub  12438  divalgmod  12675  bitsval  12691  bitsp1e  12700  bitsp1o  12701  algfx  12811  eucalgcvga  12817  reumodprminv  13013  nnnn0modprm0  13015  ballotfilemfc0  13213  ballotfilemfcc  13214  ballotfilemsima  13240  ballotfilemrv  13244  ennnfonelemex  13286  ennnfonelemhom  13287  ennnfonelemf1  13290  ennnfonelemrn  13291  ctinfomlemom  13299  ctinfom  13300  ctiunctlemudc  13309  ctiunctlemf  13310  elrest  13580  ptex  13598  imasaddfnlemg  13615  divsfval  13629  xpscf  13648  grpidvalg  13673  grpidpropdg  13674  grpidd  13683  issgrpd  13707  sgrppropd  13708  ismndd  13730  mndpropd  13733  imasmnd2  13739  imasmnd  13740  ismhm  13748  issubm  13759  imasgrp2  13893  imasgrp  13894  issubg  13956  subginv  13964  isnsg  13985  eqg0el  14012  quselbasg  14013  isghm  14026  resghm2b  14045  conjnmzb  14063  conjnsg  14064  ghmpropd  14066  imasabl  14120  gzsumsplit0  14128  prdsbasmpt  14160  prdsbasmpt2  14168  pwselbasb  14186  isrngd  14230  rngpropd  14232  imasrng  14233  qusrng  14235  rng1zrlem  14236  dfur2g  14243  srgidmlem  14259  issrgid  14262  ringcl  14294  isringid  14306  isringd  14322  imasring  14345  oppr0g  14363  oppr1g  14364  dvdsrvald  14376  isunitd  14389  unitinvcl  14406  unitinvinv  14407  unitlinv  14409  unitrinv  14410  unitnegcl  14413  dvdsrpropdg  14430  isrhm  14441  isrim0  14444  rhmmul  14447  islring  14475  opprlring  14480  issubrng  14483  opprsubrngg  14495  issubrg  14505  resrhm2b  14533  rhmpropd  14538  rrgval  14546  aprval  14567  aprap  14574  aprprop  14577  islmod  14603  lmodprop2d  14660  islssm  14669  islssmg  14670  islssmd  14671  lssats2  14726  ellspsn  14729  ixpsnbasval  14778  islidlm  14791  isridlrng  14794  rspssp  14806  rnglidlmmgm  14808  2idlval  14814  isridl  14816  2idlelb  14817  quscrng  14845  rspsn  14846  zrhval  14927  zrhrhmb  14932  znf1o  14961  psrgrp  15002  mplelbascoe  15009  istopon  15040  eltg  15079  eltg2  15080  eltop  15096  eltop2  15097  eltop3  15098  iscld  15130  neiss2  15169  isnei  15171  lmfval  15220  cnfval  15221  iscn  15224  iscnp  15226  tgcn  15235  tgcnp  15236  lmbrf  15242  cnptopresti  15265  txbas  15285  eltx  15286  txdis  15304  txdis1cn  15305  hmeofvalg  15330  ishmeo  15331  ispsmet  15350  ismet  15371  isxmet  15372  elblps  15417  elbl  15418  elmopn  15473  neibl  15518  metrest  15533  txmetcnp  15545  txmetcn  15546  metcnpd  15547  elcncf  15600  ellimc3apf  15687  limcmpted  15690  cnlimcim  15698  cnlimc  15699  eldvap  15709  dvidsslem  15720  dviaddf  15732  dvimulf  15733  elply  15761  ply1termlem  15769  lgseisenlem3  16108  edgval  16218  edgiedgbg  16223  edgupgren  16299  upgredg  16302  uhgr2edg  16364  umgr2edg1  16367  usgredg2vlem1  16380  usgredg2vlem2  16381  ushgredgedg  16384  ushgredgedgloop  16386  subgruhgredgdm  16428  uhgrspansubgrlem  16434  vtxdgfval  16446  vtxedgfi  16447  vtxdgop  16450  vtxdg0v  16452  vtxdeqd  16454  vtxdfifiun  16455  1loopgrvd0fi  16464  1hevtxdg0fi  16465  1hevtxdg1en  16466  wksfval  16480  iswlk  16481  wlkm  16497  uspgr2wlkeq  16523  wlkreslem  16536  wlkres  16537  istrl  16543  clwwlkg  16551  isclwwlk  16552  clwwlkccatlem  16558  isclwwlkng  16564  clwwlkn0  16566  clwwlknnn  16570  clwwlkext2edg  16580  clwwlknonmpo  16586  clwwlknon  16587  clwwlk0on0  16589  iseupth  16605  eupth2lem3lem3fi  16628  eupth2lem3lem6fi  16629  eupth2lem3lem4fi  16631  eupth2lembfi  16635  bj-sels  16857  pw1map  16942  nninfall  16960  nninfsellemeq  16965