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  5593  fvelrnb  5681  foelcdmi  5686  fvun1  5700  fvco2  5703  elfvmptrab1  5729  elfvmptrab  5730  elpreima  5754  dff3im  5780  resflem  5799  fmptco  5801  funfvima3  5873  foima2  5875  eluniimadm  5889  dff13  5892  f1eqcocnv  5915  isoini  5942  riotaeqdv  5955  mpoeq123dva  6065  cbvmpox  6082  ovelrn  6154  elovmpod  6203  elovmpo  6204  elovmporab  6205  elovmporab1w  6206  fmpox  6346  disjxp1  6382  opeliunxp2f  6384  mpoxopn0yelv  6385  mpoxopovel  6387  rbropapd  6388  rntpos  6403  smoel  6446  smoiso  6448  smoel2  6449  tfrlem9  6465  tfrlemisucaccv  6471  tfrlemiubacc  6476  tfrlemi14d  6479  tfri2d  6482  tfr1onlemubacc  6492  tfr1onlemres  6495  tfrcllemubacc  6505  tfrcllemres  6508  rdgon  6532  freceq1  6538  freceq2  6539  frec0g  6543  frecabcl  6545  freccllem  6548  frecfcllem  6550  frecsuclem  6552  frecsuc  6553  nnsucelsuc  6637  nnsucuniel  6641  nnmordi  6662  ereldm  6725  iinerm  6754  elmapg  6808  elpmg  6811  elixpsn  6882  ixpsnf1o  6883  pw2f1odclem  6995  phplem4  7016  phplem3g  7017  phplem4on  7029  exmidpw  7070  fiintim  7093  fidcenumlemrks  7120  fidcenumlemrk  7121  elfi  7138  ordiso2  7202  ctssdccl  7278  nnnninfeq  7295  cc2lem  7452  cc2  7453  cc3  7454  archnqq  7604  ltdfpr  7693  genpelxp  7698  genpelvl  7699  genpelvu  7700  addcanprleml  7801  addcanprlemu  7802  cauappcvgprlem1  7846  suplocexprlemell  7900  suplocexprlemmu  7905  suplocexprlemru  7906  suplocexprlemdisj  7907  suplocexprlemloc  7908  suplocexprlemub  7910  suplocexprlemlub  7911  cnm  8019  eluz1  9726  elixx1  10093  elioo2  10117  elfz1  10209  elfzp1  10268  fzpr  10273  fzsuc2  10275  fzrev3  10283  elfzp12  10295  fzm1  10296  fzoval  10344  elfzo  10345  fzodcel  10349  elfzom1b  10435  fzosplitsni  10441  nninfdcex  10457  zmodidfzo  10575  frecuzrdgtcl  10634  frecuzrdgfunlem  10641  seqf1og  10743  bcval  10971  bcpasc  10988  fundm2domnop0  11067  wrdmap  11103  elovmpowrd  11113  ccatfvalfi  11127  elfzelfzccat  11135  ccatlid  11141  ccatass  11143  ccatrn  11144  swrdfv2  11195  ccatswrd  11202  swrdccat2  11203  pfxfv  11216  pfxeq  11228  ccatpfx  11233  swrdswrd  11237  swrdpfx  11239  pfxpfx  11240  cats1un  11253  swrdccatfn  11256  swrdccatin1  11257  pfxccatin12lem4  11258  pfxccatin12lem1  11260  swrdccatin2  11261  pfxccatin12lem2c  11262  pfxccatin12lem2  11263  swrdccat3blem  11271  swrdccatin1d  11275  swrdccatin2d  11276  pfxccatin12d  11277  shftfn  11335  shftval  11336  seq3shft  11349  iser3shft  11857  sumeq1  11866  summodclem3  11891  summodclem2a  11892  isumss  11902  fsumsplit  11918  sumsplitdc  11943  fsum2dlemstep  11945  fisumcom2  11949  fsumparts  11981  explecnv  12016  fprodsplitdc  12107  fprodsplit  12108  fprod2dlemstep  12133  fprodcom2fi  12137  eftlub  12201  divalgmod  12438  bitsval  12454  bitsp1e  12463  bitsp1o  12464  algfx  12574  eucalgcvga  12580  reumodprminv  12776  nnnn0modprm0  12778  ennnfonelemex  12985  ennnfonelemhom  12986  ennnfonelemf1  12989  ennnfonelemrn  12990  ctinfomlemom  12998  ctinfom  12999  ctiunctlemudc  13008  ctiunctlemf  13009  elrest  13279  ptex  13297  prdsbasmpt  13313  prdsbasmpt2  13321  pwselbasb  13326  imasaddfnlemg  13347  divsfval  13361  xpscf  13380  grpidvalg  13406  grpidpropdg  13407  grpidd  13416  issgrpd  13445  sgrppropd  13446  ismndd  13470  mndpropd  13473  imasmnd2  13485  imasmnd  13486  ismhm  13494  issubm  13505  imasgrp2  13647  imasgrp  13648  issubg  13710  subginv  13718  isnsg  13739  eqg0el  13766  quselbasg  13767  isghm  13780  resghm2b  13799  conjnmzb  13817  conjnsg  13818  ghmpropd  13820  imasabl  13873  isrngd  13916  rngpropd  13918  imasrng  13919  qusrng  13921  dfur2g  13925  srgidmlem  13941  issrgid  13944  ringcl  13976  isringid  13988  isringd  14004  imasring  14027  oppr0g  14044  oppr1g  14045  dvdsrvald  14057  isunitd  14070  unitinvcl  14087  unitinvinv  14088  unitlinv  14090  unitrinv  14091  unitnegcl  14094  dvdsrpropdg  14111  isrhm  14122  isrim0  14125  rhmmul  14128  islring  14156  issubrng  14163  opprsubrngg  14175  issubrg  14185  resrhm2b  14213  rhmpropd  14218  rrgval  14226  aprval  14246  aprap  14250  islmod  14255  lmodprop2d  14312  islssm  14321  islssmg  14322  islssmd  14323  lssats2  14378  ellspsn  14381  ixpsnbasval  14430  islidlm  14443  isridlrng  14446  rspssp  14458  rnglidlmmgm  14460  2idlval  14466  isridl  14468  2idlelb  14469  quscrng  14497  rspsn  14498  zrhval  14581  zrhrhmb  14586  znf1o  14615  psrgrp  14649  mplelbascoe  14656  istopon  14687  eltg  14726  eltg2  14727  eltop  14743  eltop2  14744  eltop3  14745  iscld  14777  neiss2  14816  isnei  14818  lmfval  14867  cnfval  14868  iscn  14871  iscnp  14873  tgcn  14882  tgcnp  14883  lmbrf  14889  cnptopresti  14912  txbas  14932  eltx  14933  txdis  14951  txdis1cn  14952  hmeofvalg  14977  ishmeo  14978  ispsmet  14997  ismet  15018  isxmet  15019  elblps  15064  elbl  15065  elmopn  15120  neibl  15165  metrest  15180  txmetcnp  15192  txmetcn  15193  metcnpd  15194  elcncf  15247  ellimc3apf  15334  limcmpted  15337  cnlimcim  15345  cnlimc  15346  eldvap  15356  dvidsslem  15367  dviaddf  15379  dvimulf  15380  elply  15408  ply1termlem  15416  lgseisenlem3  15751  edgiedgbg  15865  edgupgren  15939  upgredg  15942  uhgr2edg  16004  umgr2edg1  16007  usgredg2vlem1  16020  usgredg2vlem2  16021  ushgredgedg  16024  ushgredgedgloop  16026  wksfval  16035  iswlk  16036  wlkm  16051  uspgr2wlkeq  16076  bj-sels  16277  2omap  16359  pw1map  16361  nninfall  16375  nninfsellemeq  16380