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  4211  axpweq  4308  rabxfrd  4615  onsucelsucexmid  4677  ordsucunielexmid  4678  0elsucexmid  4712  0nelelxp  4803  opeliunxp  4830  opeliunxp2  4920  iunxpf  4928  elrelimasn  5153  elimasng  5155  xpimasn  5236  ressn  5328  funfni  5483  fnbr  5485  fun11iun  5660  relndmfv  5728  fvelrnb  5750  foelcdmi  5755  fvun1  5769  fvco2  5774  elfvmptrab1  5801  elfvmptrab  5802  elpreima  5828  dff3im  5853  resflem  5872  fmptco  5874  funfvima3  5952  foima2  5957  eluniimadm  5971  dff13  5974  f1eqcocnv  5997  isoini  6024  riotaeqdv  6039  mpoeq123dva  6149  cbvmpox  6166  ovelrn  6238  elovmpod  6287  elovmpo  6288  elovmporab  6289  elovmporab1w  6290  fmpox  6436  disjxp1  6472  elsuppfng  6482  elsuppfn  6483  suppfnss  6497  suppcofn  6506  opeliunxp2f  6509  mpoxopn0yelv  6510  mpoxopovel  6512  rbropapd  6513  rntpos  6528  smoel  6571  smoiso  6573  smoel2  6574  tfrlem9  6590  tfrlemisucaccv  6596  tfrlemiubacc  6601  tfrlemi14d  6604  tfri2d  6607  tfr1onlemubacc  6617  tfr1onlemres  6620  tfrcllemubacc  6630  tfrcllemres  6633  rdgon  6657  freceq1  6663  freceq2  6664  frec0g  6668  frecabcl  6670  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecsuc  6678  nnsucelsuc  6764  nnsucuniel  6768  nnmordi  6789  ereldm  6852  iinerm  6881  elmapg  6935  elpmg  6938  elixpsn  7017  ixpsnf1o  7018  pw2f1odclem  7134  phplem4  7156  phplem3g  7157  phplem4on  7169  exmidpw  7215  fiintim  7238  fidcenumlemrks  7270  fidcenumlemrk  7271  elfi  7305  2omap  7318  ordiso2  7375  ctssdccl  7451  nnnninfeq  7468  cc2lem  7632  cc2  7633  cc3  7634  archnqq  7784  ltdfpr  7873  genpelxp  7878  genpelvl  7879  genpelvu  7880  addcanprleml  7981  addcanprlemu  7982  cauappcvgprlem1  8026  suplocexprlemell  8080  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemub  8090  suplocexprlemlub  8091  cnm  8199  indval0  9297  eluz1  9925  elixx1  10299  elioo2  10323  elfz1  10416  elfzp1  10479  fzpr  10484  fzsuc2  10486  fzrev3  10494  elfzp12  10506  fzm1  10507  fzoval  10555  elfzo  10556  fzodcel  10560  elfzom1b  10647  fzosplitsni  10654  nninfdcex  10672  zmodidfzo  10790  frecuzrdgtcl  10849  frecuzrdgfunlem  10856  seqf1og  10958  bcval  11187  bcpasc  11204  hashf1lem1  11285  fundm2domnop0  11300  wrdmap  11336  elovmpowrd  11346  ccatfvalfi  11360  elfzelfzccat  11368  ccatlid  11374  ccatass  11376  ccatrn  11377  ccatalpha  11381  swrdfv2  11435  ccatswrd  11442  swrdccat2  11443  pfxfv  11456  pfxeq  11468  ccatpfx  11473  swrdswrd  11477  swrdpfx  11479  pfxpfx  11480  cats1un  11493  swrdccatfn  11496  swrdccatin1  11497  pfxccatin12lem4  11498  pfxccatin12lem1  11500  swrdccatin2  11501  pfxccatin12lem2c  11502  pfxccatin12lem2  11503  swrdccat3blem  11511  swrdccatin1d  11515  swrdccatin2d  11516  pfxccatin12d  11517  shftfn  11589  shftval  11590  seq3shft  11603  iser3shft  12112  sumeq1  12121  summodclem3  12147  summodclem2a  12148  isumss  12158  fsumsplit  12174  sumsplitdc  12199  fsum2dlemstep  12201  fisumcom2  12205  fsumparts  12237  explecnv  12272  fprodsplitdc  12363  fprodsplit  12364  fprod2dlemstep  12389  fprodcom2fi  12393  eftlub  12457  divalgmod  12694  bitsval  12710  bitsp1e  12719  bitsp1o  12720  algfx  12830  eucalgcvga  12836  reumodprminv  13032  nnnn0modprm0  13034  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemsima  13259  ballotfilemrv  13263  ennnfonelemex  13305  ennnfonelemhom  13306  ennnfonelemf1  13309  ennnfonelemrn  13310  ctinfomlemom  13318  ctinfom  13319  ctiunctlemudc  13328  ctiunctlemf  13329  elrest  13600  ptex  13618  imasaddfnlemg  13635  divsfval  13649  xpscf  13668  grpidvalg  13693  grpidpropdg  13694  grpidd  13703  issgrpd  13727  sgrppropd  13728  ismndd  13750  mndpropd  13753  imasmnd2  13759  imasmnd  13760  ismhm  13768  issubm  13779  imasgrp2  13913  imasgrp  13914  issubg  13976  subginv  13984  isnsg  14005  eqg0el  14032  quselbasg  14033  isghm  14046  resghm2b  14065  conjnmzb  14083  conjnsg  14084  ghmpropd  14086  imasabl  14140  gzsumsplit0  14148  prdsbasmpt  14180  prdsbasmpt2  14188  pwselbasb  14206  mgpplusg  14222  mgpbas  14225  isrngd  14252  rngpropd  14254  imasrng  14255  qusrng  14257  rng1zrlem  14258  ringidval  14265  dfur2g  14266  srgidmlem  14282  issrgid  14285  ringcl  14317  isringid  14330  isringd  14346  imasring  14369  oppr0g  14387  oppr1g  14388  dvdsrvald  14400  isunitd  14413  unitinvcl  14430  unitinvinv  14431  unitlinv  14433  unitrinv  14434  unitnegcl  14437  dvdsrpropdg  14454  isrhm  14465  isrim0  14468  rhmmul  14471  islring  14499  opprlring  14504  issubrng  14507  opprsubrngg  14519  issubrg  14529  resrhm2b  14557  rhmpropd  14562  rrgval  14570  aprval  14591  aprap  14598  aprprop  14601  islmod  14627  lmodprop2d  14685  islssm  14694  islssmg  14695  islssmd  14696  lssats2  14751  ellspsn  14754  ixpsnbasval  14803  islidlm  14816  isridlrng  14819  rspssp  14831  rnglidlmmgm  14833  2idlval  14839  isridl  14841  2idlelb  14842  quscrng  14870  rspsn  14871  zrhval  14952  zrhrhmb  14957  znf1o  14986  asclfval  15021  assamulgscmlem2  15042  psrgrp  15076  mplelbascoe  15083  istopon  15114  eltg  15153  eltg2  15154  eltop  15170  eltop2  15171  eltop3  15172  iscld  15204  neiss2  15243  isnei  15245  lmfval  15294  cnfval  15295  iscn  15298  iscnp  15300  tgcn  15309  tgcnp  15310  lmbrf  15316  cnptopresti  15339  txbas  15359  eltx  15360  txdis  15378  txdis1cn  15379  hmeofvalg  15404  ishmeo  15405  ispsmet  15424  ismet  15445  isxmet  15446  elblps  15491  elbl  15492  elmopn  15547  neibl  15592  metrest  15607  txmetcnp  15619  txmetcn  15620  metcnpd  15621  elcncf  15674  ellimc3apf  15761  limcmpted  15764  cnlimcim  15772  cnlimc  15773  eldvap  15783  dvidsslem  15794  dviaddf  15806  dvimulf  15807  elply  15835  ply1termlem  15843  lgseisenlem3  16191  edgval  16301  edgiedgbg  16306  edgupgren  16382  upgredg  16385  uhgr2edg  16447  umgr2edg1  16450  usgredg2vlem1  16463  usgredg2vlem2  16464  ushgredgedg  16467  ushgredgedgloop  16469  subgruhgredgdm  16511  uhgrspansubgrlem  16517  vtxdgfval  16529  vtxedgfi  16530  vtxdgop  16533  vtxdg0v  16535  vtxdeqd  16537  vtxdfifiun  16538  1loopgrvd0fi  16547  1hevtxdg0fi  16548  1hevtxdg1en  16549  wksfval  16563  iswlk  16564  wlkm  16580  uspgr2wlkeq  16606  wlkreslem  16619  wlkres  16620  istrl  16626  clwwlkg  16634  isclwwlk  16635  clwwlkccatlem  16641  isclwwlkng  16647  clwwlkn0  16649  clwwlknnn  16653  clwwlkext2edg  16663  clwwlknonmpo  16669  clwwlknon  16670  clwwlk0on0  16672  iseupth  16688  eupth2lem3lem3fi  16711  eupth2lem3lem6fi  16712  eupth2lem3lem4fi  16714  eupth2lembfi  16718  bj-sels  16940  pw1map  17025  wexmiddiffilem  17043  wexmiddifxylem  17045  nninfall  17052  nninfsellemeq  17057