Theorem eleq2d 2301

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 2295	. 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 1397   e. wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eleq12d  2302  eleqtrd  2310  neleqtrd  2329  neleqtrrd  2330  abeq2d  2344  nfceqdf  2373  drnfc1  2391  drnfc2  2392  sbcbid  3089  cbvcsbw  3131  cbvcsb  3132  sbcel1g  3146  csbeq2d  3152  csbie2g  3178  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  rabsnif  3738  opeq1  3862  opeq2  3863  cbviun  4007  cbviin  4008  iinxsng  4044  iinxprg  4045  iunxsng  4046  iunxsngf  4048  cbvdisj  4074  disjnim  4078  disjiun  4083  mpteq12f  4169  axpweq  4261  rabxfrd  4566  onsucelsucexmid  4628  ordsucunielexmid  4629  0elsucexmid  4663  0nelelxp  4754  opeliunxp  4781  opeliunxp2  4870  iunxpf  4878  elrelimasn  5102  elimasng  5104  xpimasn  5185  ressn  5277  funfni  5432  fnbr  5434  fun11iun  5605  fvelrnb  5694  foelcdmi  5699  fvun1  5713  fvco2  5716  elfvmptrab1  5742  elfvmptrab  5743  elpreima  5767  dff3im  5793  resflem  5812  fmptco  5814  funfvima3  5891  foima2  5895  eluniimadm  5909  dff13  5912  f1eqcocnv  5935  isoini  5962  riotaeqdv  5975  mpoeq123dva  6085  cbvmpox  6102  ovelrn  6174  elovmpod  6223  elovmpo  6224  elovmporab  6225  elovmporab1w  6226  fmpox  6368  disjxp1  6404  opeliunxp2f  6407  mpoxopn0yelv  6408  mpoxopovel  6410  rbropapd  6411  rntpos  6426  smoel  6469  smoiso  6471  smoel2  6472  tfrlem9  6488  tfrlemisucaccv  6494  tfrlemiubacc  6499  tfrlemi14d  6502  tfri2d  6505  tfr1onlemubacc  6515  tfr1onlemres  6518  tfrcllemubacc  6528  tfrcllemres  6531  rdgon  6555  freceq1  6561  freceq2  6562  frec0g  6566  frecabcl  6568  freccllem  6571  frecfcllem  6573  frecsuclem  6575  frecsuc  6576  nnsucelsuc  6662  nnsucuniel  6666  nnmordi  6687  ereldm  6750  iinerm  6779  elmapg  6833  elpmg  6836  elixpsn  6907  ixpsnf1o  6908  pw2f1odclem  7023  phplem4  7044  phplem3g  7045  phplem4on  7057  exmidpw  7103  fiintim  7126  fidcenumlemrks  7155  fidcenumlemrk  7156  elfi  7173  ordiso2  7237  ctssdccl  7313  nnnninfeq  7330  cc2lem  7488  cc2  7489  cc3  7490  archnqq  7640  ltdfpr  7729  genpelxp  7734  genpelvl  7735  genpelvu  7736  addcanprleml  7837  addcanprlemu  7838  cauappcvgprlem1  7882  suplocexprlemell  7936  suplocexprlemmu  7941  suplocexprlemru  7942  suplocexprlemdisj  7943  suplocexprlemloc  7944  suplocexprlemub  7946  suplocexprlemlub  7947  cnm  8055  eluz1  9762  elixx1  10135  elioo2  10159  elfz1  10251  elfzp1  10310  fzpr  10315  fzsuc2  10317  fzrev3  10325  elfzp12  10337  fzm1  10338  fzoval  10386  elfzo  10387  fzodcel  10391  elfzom1b  10478  fzosplitsni  10485  nninfdcex  10501  zmodidfzo  10619  frecuzrdgtcl  10678  frecuzrdgfunlem  10685  seqf1og  10787  bcval  11015  bcpasc  11032  fundm2domnop0  11116  wrdmap  11152  elovmpowrd  11162  ccatfvalfi  11176  elfzelfzccat  11184  ccatlid  11190  ccatass  11192  ccatrn  11193  ccatalpha  11197  swrdfv2  11251  ccatswrd  11258  swrdccat2  11259  pfxfv  11272  pfxeq  11284  ccatpfx  11289  swrdswrd  11293  swrdpfx  11295  pfxpfx  11296  cats1un  11309  swrdccatfn  11312  swrdccatin1  11313  pfxccatin12lem4  11314  pfxccatin12lem1  11316  swrdccatin2  11317  pfxccatin12lem2c  11318  pfxccatin12lem2  11319  swrdccat3blem  11327  swrdccatin1d  11331  swrdccatin2d  11332  pfxccatin12d  11333  shftfn  11405  shftval  11406  seq3shft  11419  iser3shft  11927  sumeq1  11936  summodclem3  11962  summodclem2a  11963  isumss  11973  fsumsplit  11989  sumsplitdc  12014  fsum2dlemstep  12016  fisumcom2  12020  fsumparts  12052  explecnv  12087  fprodsplitdc  12178  fprodsplit  12179  fprod2dlemstep  12204  fprodcom2fi  12208  eftlub  12272  divalgmod  12509  bitsval  12525  bitsp1e  12534  bitsp1o  12535  algfx  12645  eucalgcvga  12651  reumodprminv  12847  nnnn0modprm0  12849  ennnfonelemex  13056  ennnfonelemhom  13057  ennnfonelemf1  13060  ennnfonelemrn  13061  ctinfomlemom  13069  ctinfom  13070  ctiunctlemudc  13079  ctiunctlemf  13080  elrest  13350  ptex  13368  prdsbasmpt  13384  prdsbasmpt2  13392  pwselbasb  13397  imasaddfnlemg  13418  divsfval  13432  xpscf  13451  grpidvalg  13477  grpidpropdg  13478  grpidd  13487  issgrpd  13516  sgrppropd  13517  ismndd  13541  mndpropd  13544  imasmnd2  13556  imasmnd  13557  ismhm  13565  issubm  13576  imasgrp2  13718  imasgrp  13719  issubg  13781  subginv  13789  isnsg  13810  eqg0el  13837  quselbasg  13838  isghm  13851  resghm2b  13870  conjnmzb  13888  conjnsg  13889  ghmpropd  13891  imasabl  13944  gsumsplit0  13954  isrngd  13988  rngpropd  13990  imasrng  13991  qusrng  13993  dfur2g  13997  srgidmlem  14013  issrgid  14016  ringcl  14048  isringid  14060  isringd  14076  imasring  14099  oppr0g  14116  oppr1g  14117  dvdsrvald  14129  isunitd  14142  unitinvcl  14159  unitinvinv  14160  unitlinv  14162  unitrinv  14163  unitnegcl  14166  dvdsrpropdg  14183  isrhm  14194  isrim0  14197  rhmmul  14200  islring  14228  issubrng  14235  opprsubrngg  14247  issubrg  14257  resrhm2b  14285  rhmpropd  14290  rrgval  14298  aprval  14318  aprap  14322  islmod  14327  lmodprop2d  14384  islssm  14393  islssmg  14394  islssmd  14395  lssats2  14450  ellspsn  14453  ixpsnbasval  14502  islidlm  14515  isridlrng  14518  rspssp  14530  rnglidlmmgm  14532  2idlval  14538  isridl  14540  2idlelb  14541  quscrng  14569  rspsn  14570  zrhval  14653  zrhrhmb  14658  znf1o  14687  psrgrp  14726  mplelbascoe  14733  istopon  14764  eltg  14803  eltg2  14804  eltop  14820  eltop2  14821  eltop3  14822  iscld  14854  neiss2  14893  isnei  14895  lmfval  14944  cnfval  14945  iscn  14948  iscnp  14950  tgcn  14959  tgcnp  14960  lmbrf  14966  cnptopresti  14989  txbas  15009  eltx  15010  txdis  15028  txdis1cn  15029  hmeofvalg  15054  ishmeo  15055  ispsmet  15074  ismet  15095  isxmet  15096  elblps  15141  elbl  15142  elmopn  15197  neibl  15242  metrest  15257  txmetcnp  15269  txmetcn  15270  metcnpd  15271  elcncf  15324  ellimc3apf  15411  limcmpted  15414  cnlimcim  15422  cnlimc  15423  eldvap  15433  dvidsslem  15444  dviaddf  15456  dvimulf  15457  elply  15485  ply1termlem  15493  lgseisenlem3  15828  edgval  15938  edgiedgbg  15943  edgupgren  16019  upgredg  16022  uhgr2edg  16084  umgr2edg1  16087  usgredg2vlem1  16100  usgredg2vlem2  16101  ushgredgedg  16104  ushgredgedgloop  16106  subgruhgredgdm  16148  uhgrspansubgrlem  16154  vtxdgfval  16166  vtxedgfi  16167  vtxdgop  16170  vtxdg0v  16172  vtxdeqd  16174  vtxdfifiun  16175  1loopgrvd0fi  16184  1hevtxdg0fi  16185  1hevtxdg1en  16186  wksfval  16200  iswlk  16201  wlkm  16217  uspgr2wlkeq  16243  wlkreslem  16256  wlkres  16257  istrl  16263  clwwlkg  16271  isclwwlk  16272  clwwlkccatlem  16278  isclwwlkng  16284  clwwlkn0  16286  clwwlknnn  16290  clwwlkext2edg  16300  clwwlknonmpo  16306  clwwlknon  16307  clwwlk0on0  16309  iseupth  16325  eupth2lem3lem3fi  16348  eupth2lem3lem6fi  16349  eupth2lem3lem4fi  16351  eupth2lembfi  16355  bj-sels  16568  2omap  16653  pw1map  16655  nninfall  16670  nninfsellemeq  16675