Theorem eleq2d 2275

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 2269	. 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 1373   e. wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  eleq12d  2276  eleqtrd  2284  neleqtrd  2303  neleqtrrd  2304  abeq2d  2318  nfceqdf  2347  drnfc1  2365  drnfc2  2366  sbcbid  3056  cbvcsbw  3097  cbvcsb  3098  sbcel1g  3112  csbeq2d  3118  csbie2g  3144  cbvralcsf  3156  cbvrexcsf  3157  cbvreucsf  3158  cbvrabcsf  3159  opeq1  3819  opeq2  3820  cbviun  3964  cbviin  3965  iinxsng  4001  iinxprg  4002  iunxsng  4003  iunxsngf  4005  cbvdisj  4031  disjnim  4035  disjiun  4040  mpteq12f  4125  axpweq  4216  rabxfrd  4517  onsucelsucexmid  4579  ordsucunielexmid  4580  0elsucexmid  4614  0nelelxp  4705  opeliunxp  4731  opeliunxp2  4819  iunxpf  4827  elrelimasn  5049  elimasng  5051  xpimasn  5132  ressn  5224  funfni  5377  fnbr  5379  fun11iun  5545  fvelrnb  5628  foelcdmi  5633  fvun1  5647  fvco2  5650  elfvmptrab1  5676  elfvmptrab  5677  elpreima  5701  dff3im  5727  resflem  5746  fmptco  5748  funfvima3  5820  foima2  5822  eluniimadm  5836  dff13  5839  f1eqcocnv  5862  isoini  5889  riotaeqdv  5902  mpoeq123dva  6008  cbvmpox  6025  ovelrn  6097  elovmpod  6146  elovmpo  6147  elovmporab  6148  elovmporab1w  6149  fmpox  6288  disjxp1  6324  opeliunxp2f  6326  mpoxopn0yelv  6327  mpoxopovel  6329  rbropapd  6330  rntpos  6345  smoel  6388  smoiso  6390  smoel2  6391  tfrlem9  6407  tfrlemisucaccv  6413  tfrlemiubacc  6418  tfrlemi14d  6421  tfri2d  6424  tfr1onlemubacc  6434  tfr1onlemres  6437  tfrcllemubacc  6447  tfrcllemres  6450  rdgon  6474  freceq1  6480  freceq2  6481  frec0g  6485  frecabcl  6487  freccllem  6490  frecfcllem  6492  frecsuclem  6494  frecsuc  6495  nnsucelsuc  6579  nnsucuniel  6583  nnmordi  6604  ereldm  6667  iinerm  6696  elmapg  6750  elpmg  6753  elixpsn  6824  ixpsnf1o  6825  pw2f1odclem  6933  phplem4  6954  phplem3g  6955  phplem4on  6966  exmidpw  7007  fiintim  7030  fidcenumlemrks  7057  fidcenumlemrk  7058  elfi  7075  ordiso2  7139  ctssdccl  7215  nnnninfeq  7232  cc2lem  7380  cc2  7381  cc3  7382  archnqq  7532  ltdfpr  7621  genpelxp  7626  genpelvl  7627  genpelvu  7628  addcanprleml  7729  addcanprlemu  7730  cauappcvgprlem1  7774  suplocexprlemell  7828  suplocexprlemmu  7833  suplocexprlemru  7834  suplocexprlemdisj  7835  suplocexprlemloc  7836  suplocexprlemub  7838  suplocexprlemlub  7839  cnm  7947  eluz1  9654  elixx1  10021  elioo2  10045  elfz1  10137  elfzp1  10196  fzpr  10201  fzsuc2  10203  fzrev3  10211  elfzp12  10223  fzm1  10224  fzoval  10272  elfzo  10273  fzodcel  10277  elfzom1b  10360  fzosplitsni  10366  nninfdcex  10382  zmodidfzo  10500  frecuzrdgtcl  10559  frecuzrdgfunlem  10566  seqf1og  10668  bcval  10896  bcpasc  10913  fundm2domnop0  10992  wrdmap  11027  elovmpowrd  11037  ccatfvalfi  11051  elfzelfzccat  11059  ccatlid  11065  ccatass  11067  ccatrn  11068  swrdfv2  11119  ccatswrd  11126  swrdccat2  11127  pfxfv  11138  pfxeq  11150  ccatpfx  11155  shftfn  11168  shftval  11169  seq3shft  11182  iser3shft  11690  sumeq1  11699  summodclem3  11724  summodclem2a  11725  isumss  11735  fsumsplit  11751  sumsplitdc  11776  fsum2dlemstep  11778  fisumcom2  11782  fsumparts  11814  explecnv  11849  fprodsplitdc  11940  fprodsplit  11941  fprod2dlemstep  11966  fprodcom2fi  11970  eftlub  12034  divalgmod  12271  bitsval  12287  bitsp1e  12296  bitsp1o  12297  algfx  12407  eucalgcvga  12413  reumodprminv  12609  nnnn0modprm0  12611  ennnfonelemex  12818  ennnfonelemhom  12819  ennnfonelemf1  12822  ennnfonelemrn  12823  ctinfomlemom  12831  ctinfom  12832  ctiunctlemudc  12841  ctiunctlemf  12842  elrest  13111  ptex  13129  prdsbasmpt  13145  prdsbasmpt2  13153  pwselbasb  13158  imasaddfnlemg  13179  divsfval  13193  xpscf  13212  grpidvalg  13238  grpidpropdg  13239  grpidd  13248  issgrpd  13277  sgrppropd  13278  ismndd  13302  mndpropd  13305  imasmnd2  13317  imasmnd  13318  ismhm  13326  issubm  13337  imasgrp2  13479  imasgrp  13480  issubg  13542  subginv  13550  isnsg  13571  eqg0el  13598  quselbasg  13599  isghm  13612  resghm2b  13631  conjnmzb  13649  conjnsg  13650  ghmpropd  13652  imasabl  13705  isrngd  13748  rngpropd  13750  imasrng  13751  qusrng  13753  dfur2g  13757  srgidmlem  13773  issrgid  13776  ringcl  13808  isringid  13820  isringd  13836  imasring  13859  oppr0g  13876  oppr1g  13877  reldvdsrsrg  13887  dvdsrvald  13888  isunitd  13901  unitinvcl  13918  unitinvinv  13919  unitlinv  13921  unitrinv  13922  unitnegcl  13925  dvdsrpropdg  13942  isrhm  13953  isrim0  13956  rhmmul  13959  islring  13987  issubrng  13994  opprsubrngg  14006  issubrg  14016  resrhm2b  14044  rhmpropd  14049  rrgval  14057  aprval  14077  aprap  14081  islmod  14086  lmodprop2d  14143  islssm  14152  islssmg  14153  islssmd  14154  lssats2  14209  ellspsn  14212  ixpsnbasval  14261  islidlm  14274  isridlrng  14277  rspssp  14289  rnglidlmmgm  14291  2idlval  14297  isridl  14299  2idlelb  14300  quscrng  14328  rspsn  14329  zrhval  14412  zrhrhmb  14417  znf1o  14446  psrgrp  14480  mplelbascoe  14487  istopon  14518  eltg  14557  eltg2  14558  eltop  14574  eltop2  14575  eltop3  14576  iscld  14608  neiss2  14647  isnei  14649  lmfval  14697  cnfval  14699  iscn  14702  iscnp  14704  tgcn  14713  tgcnp  14714  lmbrf  14720  cnptopresti  14743  txbas  14763  eltx  14764  txdis  14782  txdis1cn  14783  hmeofvalg  14808  ishmeo  14809  ispsmet  14828  ismet  14849  isxmet  14850  elblps  14895  elbl  14896  elmopn  14951  neibl  14996  metrest  15011  txmetcnp  15023  txmetcn  15024  metcnpd  15025  elcncf  15078  ellimc3apf  15165  limcmpted  15168  cnlimcim  15176  cnlimc  15177  eldvap  15187  dvidsslem  15198  dviaddf  15210  dvimulf  15211  elply  15239  ply1termlem  15247  lgseisenlem3  15582  edgiedgbg  15692  bj-sels  15887  2omap  15969  nninfall  15983  nninfsellemeq  15988