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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   e. wcel 2209

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used 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  3778  opeq1  3904  opeq2  3905  cbviun  4049  cbviin  4050  iinxsng  4086  iinxprg  4087  iunxsng  4088  iunxsngf  4090  cbvdisj  4116  disjnim  4120  disjiun  4125  mpteq12f  4212  axpweq  4310  rabxfrd  4617  onsucelsucexmid  4679  ordsucunielexmid  4680  0elsucexmid  4714  0nelelxp  4805  opeliunxp  4832  opeliunxp2  4922  iunxpf  4930  elrelimasn  5156  elimasng  5158  xpimasn  5239  ressn  5331  funfni  5486  fnbr  5488  fun11iun  5663  relndmfv  5731  fvelrnb  5753  foelcdmi  5758  fvun1  5772  fvco2  5777  elfvmptrab1  5804  elfvmptrab  5805  elpreima  5831  dff3im  5856  resflem  5875  fmptco  5877  funfvima3  5955  foima2  5960  eluniimadm  5974  dff13  5977  f1eqcocnv  6000  isoini  6027  riotaeqdv  6042  mpoeq123dva  6152  cbvmpox  6169  ovelrn  6241  elovmpod  6290  elovmpo  6291  elovmporab  6292  elovmporab1w  6293  fmpox  6440  disjxp1  6476  elsuppfng  6486  elsuppfn  6487  suppfnss  6501  suppcofn  6510  opeliunxp2f  6514  mpoxopn0yelv  6515  mpoxopovel  6517  rbropapd  6518  rntpos  6533  smoel  6576  smoiso  6578  smoel2  6579  tfrlem9  6595  tfrlemisucaccv  6601  tfrlemiubacc  6606  tfrlemi14d  6609  tfri2d  6612  tfr1onlemubacc  6622  tfr1onlemres  6625  tfrcllemubacc  6635  tfrcllemres  6638  rdgon  6662  freceq1  6668  freceq2  6669  frec0g  6673  frecabcl  6675  freccllem  6678  frecfcllem  6680  frecsuclem  6682  frecsuc  6683  nnsucelsuc  6769  nnsucuniel  6773  nnmordi  6794  ereldm  6857  iinerm  6886  elmapg  6940  elpmg  6943  elixpsn  7023  ixpsnf1o  7024  pw2f1odclem  7140  phplem4  7162  phplem3g  7163  phplem4on  7175  exmidpw  7221  fiintim  7244  fidcenumlemrks  7277  fidcenumlemrk  7278  elfi  7310  2omap  7324  ordiso2  7381  ctssdccl  7457  nnnninfeq  7474  cc2lem  7638  cc2  7639  cc3  7640  archnqq  7790  ltdfpr  7879  genpelxp  7884  genpelvl  7885  genpelvu  7886  addcanprleml  7987  addcanprlemu  7988  cauappcvgprlem1  8032  suplocexprlemell  8086  suplocexprlemmu  8091  suplocexprlemru  8092  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemub  8096  suplocexprlemlub  8097  cnm  8205  indval0  9306  eluz1  9940  elixx1  10315  elioo2  10339  elfz1  10432  elfzp1  10495  fzpr  10500  fzsuc2  10502  fzrev3  10510  elfzp12  10522  fzm1  10523  fzoval  10571  elfzo  10572  fzodcel  10576  elfzom1b  10663  fzosplitsni  10670  nninfdcex  10688  zmodidfzo  10810  frecuzrdgtcl  10869  frecuzrdgfunlem  10876  seqf1og  10978  bcval  11208  bcpasc  11225  hashf1lem1  11306  fundm2domnop0  11321  wrdmap  11357  elovmpowrd  11367  ccatfvalfi  11381  elfzelfzccat  11389  ccatlid  11395  ccatass  11397  ccatrn  11398  ccatalpha  11402  swrdfv2  11456  ccatswrd  11463  swrdccat2  11464  pfxfv  11477  pfxeq  11489  ccatpfx  11494  swrdswrd  11498  swrdpfx  11500  pfxpfx  11501  cats1un  11514  swrdccatfn  11517  swrdccatin1  11518  pfxccatin12lem4  11519  pfxccatin12lem1  11521  swrdccatin2  11522  pfxccatin12lem2c  11523  pfxccatin12lem2  11524  swrdccat3blem  11532  swrdccatin1d  11536  swrdccatin2d  11537  pfxccatin12d  11538  shftfn  11610  shftval  11611  seq3shft  11624  iser3shft  12136  sumeq1  12145  summodclem3  12171  summodclem2a  12172  isumss  12182  fsumsplit  12198  sumsplitdc  12223  fsum2dlemstep  12225  fisumcom2  12229  fsumparts  12261  explecnv  12296  fprodsplitdc  12387  fprodsplit  12388  fprod2dlemstep  12413  fprodcom2fi  12417  eftlub  12481  divalgmod  12718  bitsval  12734  bitsp1e  12743  bitsp1o  12744  algfx  12854  eucalgcvga  12860  reumodprminv  13060  nnnn0modprm0  13062  prmlem0  13248  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemsima  13316  ballotfilemrv  13320  ennnfonelemex  13362  ennnfonelemhom  13363  ennnfonelemf1  13366  ennnfonelemrn  13367  ctinfomlemom  13375  ctinfom  13376  ctiunctlemudc  13385  ctiunctlemf  13386  elrest  13658  ptex  13676  imasaddfnlemg  13693  divsfval  13707  xpscf  13726  grpidvalg  13751  grpidpropdg  13752  grpidd  13761  issgrpd  13785  sgrppropd  13786  ismndd  13808  mndpropd  13811  imasmnd2  13817  imasmnd  13818  ismhm  13826  issubm  13837  imasgrp2  13971  imasgrp  13972  issubg  14034  subginv  14042  isnsg  14063  eqg0el  14090  quselbasg  14091  isghm  14104  resghm2b  14123  conjnmzb  14141  conjnsg  14142  ghmpropd  14144  cntrval  14150  cntzval  14152  elcntz  14153  elcntzsn  14156  resscntz  14165  imasabl  14229  gzsumsplit0  14237  gsummptfidmsplit  14253  prdsbasmpt  14286  prdsbasmpt2  14294  pwselbasb  14312  mgpplusg  14328  mgpbas  14331  isrngd  14358  rngpropd  14360  imasrng  14361  qusrng  14363  rng1zrlem  14364  ringidval  14371  dfur2g  14372  srgidmlem  14388  issrgid  14391  ringcl  14423  isringid  14436  isringd  14452  imasring  14477  oppr0g  14495  oppr1g  14496  dvdsrvald  14508  isunitd  14521  unitinvcl  14538  unitinvinv  14539  unitlinv  14541  unitrinv  14542  unitnegcl  14545  dvdsrpropdg  14562  isrhm  14573  isrim0  14576  rhmmul  14579  islring  14607  opprlring  14612  issubrng  14615  opprsubrngg  14627  issubrg  14637  resrhm2b  14665  rhmpropd  14670  rrgval  14678  aprval  14699  aprap  14706  aprprop  14709  islmod  14735  lmodprop2d  14793  islssm  14802  islssmg  14803  islssmd  14804  lssats2  14859  ellspsn  14862  ixpsnbasval  14911  islidlm  14924  isridlrng  14927  rspssp  14939  rnglidlmmgm  14941  2idlval  14947  isridl  14949  2idlelb  14950  quscrng  14978  rspsn  14979  zrhval  15060  zrhrhmb  15065  znf1o  15094  asclfval  15129  assamulgscmlem2  15150  psrgrp  15204  mplbas  15223  mvrclfi  15226  mplsubgfilemcl  15232  istopon  15256  eltg  15295  eltg2  15296  eltop  15312  eltop2  15313  eltop3  15314  iscld  15346  neiss2  15385  isnei  15387  lmfval  15436  cnfval  15437  iscn  15440  iscnp  15442  tgcn  15451  tgcnp  15452  lmbrf  15458  cnptopresti  15481  txbas  15501  eltx  15502  txdis  15520  txdis1cn  15521  hmeofvalg  15546  ishmeo  15547  ispsmet  15566  ismet  15587  isxmet  15588  elblps  15633  elbl  15634  elmopn  15689  neibl  15734  metrest  15749  txmetcnp  15761  txmetcn  15762  metcnpd  15763  elcncf  15816  ellimc3apf  15903  limcmpted  15906  cnlimcim  15914  cnlimc  15915  eldvap  15925  dvidsslem  15936  dviaddf  15948  dvimulf  15949  elply  15977  ply1termlem  15985  lgseisenlem3  16413  edgval  16523  edgiedgbg  16528  edgupgren  16604  upgredg  16607  uhgr2edg  16669  umgr2edg1  16672  usgredg2vlem1  16685  usgredg2vlem2  16686  ushgredgedg  16689  ushgredgedgloop  16691  subgruhgredgdm  16733  uhgrspansubgrlem  16739  vtxdgfval  16751  vtxedgfi  16752  vtxdgop  16755  vtxdg0v  16757  vtxdeqd  16759  vtxdfifiun  16760  1loopgrvd0fi  16769  1hevtxdg0fi  16770  1hevtxdg1en  16771  wksfval  16785  iswlk  16786  wlkm  16802  uspgr2wlkeq  16828  wlkreslem  16841  wlkres  16842  istrl  16848  clwwlkg  16856  isclwwlk  16857  clwwlkccatlem  16863  isclwwlkng  16869  clwwlkn0  16871  clwwlknnn  16875  clwwlkext2edg  16885  clwwlknonmpo  16891  clwwlknon  16892  clwwlk0on0  16894  iseupth  16910  eupth2lem3lem3fi  16933  eupth2lem3lem6fi  16934  eupth2lem3lem4fi  16936  eupth2lembfi  16940  bj-sels  17162  pw1map  17247  wexmiddiffilem  17265  wexmiddifxylem  17267  nninfall  17275  nninfsellemeq  17280