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  6513  mpoxopn0yelv  6514  mpoxopovel  6516  rbropapd  6517  rntpos  6532  smoel  6575  smoiso  6577  smoel2  6578  tfrlem9  6594  tfrlemisucaccv  6600  tfrlemiubacc  6605  tfrlemi14d  6608  tfri2d  6611  tfr1onlemubacc  6621  tfr1onlemres  6624  tfrcllemubacc  6634  tfrcllemres  6637  rdgon  6661  freceq1  6667  freceq2  6668  frec0g  6672  frecabcl  6674  freccllem  6677  frecfcllem  6679  frecsuclem  6681  frecsuc  6682  nnsucelsuc  6768  nnsucuniel  6772  nnmordi  6793  ereldm  6856  iinerm  6885  elmapg  6939  elpmg  6942  elixpsn  7021  ixpsnf1o  7022  pw2f1odclem  7138  phplem4  7160  phplem3g  7161  phplem4on  7173  exmidpw  7219  fiintim  7242  fidcenumlemrks  7275  fidcenumlemrk  7276  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  9941  elixx1  10316  elioo2  10340  elfz1  10433  elfzp1  10496  fzpr  10501  fzsuc2  10503  fzrev3  10511  elfzp12  10523  fzm1  10524  fzoval  10572  elfzo  10573  fzodcel  10577  elfzom1b  10664  fzosplitsni  10671  nninfdcex  10689  zmodidfzo  10811  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  seqf1og  10979  bcval  11209  bcpasc  11226  hashf1lem1  11307  fundm2domnop0  11322  wrdmap  11358  elovmpowrd  11368  ccatfvalfi  11382  elfzelfzccat  11390  ccatlid  11396  ccatass  11398  ccatrn  11399  ccatalpha  11403  swrdfv2  11457  ccatswrd  11464  swrdccat2  11465  pfxfv  11478  pfxeq  11490  ccatpfx  11495  swrdswrd  11499  swrdpfx  11501  pfxpfx  11502  cats1un  11515  swrdccatfn  11518  swrdccatin1  11519  pfxccatin12lem4  11520  pfxccatin12lem1  11522  swrdccatin2  11523  pfxccatin12lem2c  11524  pfxccatin12lem2  11525  swrdccat3blem  11533  swrdccatin1d  11537  swrdccatin2d  11538  pfxccatin12d  11539  shftfn  11611  shftval  11612  seq3shft  11625  iser3shft  12137  sumeq1  12146  summodclem3  12172  summodclem2a  12173  isumss  12183  fsumsplit  12199  sumsplitdc  12224  fsum2dlemstep  12226  fisumcom2  12230  fsumparts  12262  explecnv  12297  fprodsplitdc  12388  fprodsplit  12389  fprod2dlemstep  12414  fprodcom2fi  12418  eftlub  12482  divalgmod  12719  bitsval  12735  bitsp1e  12744  bitsp1o  12745  algfx  12855  eucalgcvga  12861  reumodprminv  13061  nnnn0modprm0  13063  prmlem0  13249  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemsima  13317  ballotfilemrv  13321  ennnfonelemex  13363  ennnfonelemhom  13364  ennnfonelemf1  13367  ennnfonelemrn  13368  ctinfomlemom  13376  ctinfom  13377  ctiunctlemudc  13386  ctiunctlemf  13387  elrest  13659  ptex  13677  imasaddfnlemg  13694  divsfval  13708  xpscf  13727  grpidvalg  13752  grpidpropdg  13753  grpidd  13762  issgrpd  13786  sgrppropd  13787  ismndd  13809  mndpropd  13812  imasmnd2  13818  imasmnd  13819  ismhm  13827  issubm  13838  imasgrp2  13972  imasgrp  13973  issubg  14035  subginv  14043  isnsg  14064  eqg0el  14091  quselbasg  14092  isghm  14105  resghm2b  14124  conjnmzb  14142  conjnsg  14143  ghmpropd  14145  cntrval  14151  cntzval  14153  elcntz  14154  elcntzsn  14157  resscntz  14166  imasabl  14230  gzsumsplit0  14238  gsummptfidmsplit  14254  prdsbasmpt  14287  prdsbasmpt2  14295  pwselbasb  14313  mgpplusg  14329  mgpbas  14332  isrngd  14359  rngpropd  14361  imasrng  14362  qusrng  14364  rng1zrlem  14365  ringidval  14372  dfur2g  14373  srgidmlem  14389  issrgid  14392  ringcl  14424  isringid  14437  isringd  14453  imasring  14478  oppr0g  14496  oppr1g  14497  dvdsrvald  14509  isunitd  14522  unitinvcl  14539  unitinvinv  14540  unitlinv  14542  unitrinv  14543  unitnegcl  14546  dvdsrpropdg  14563  isrhm  14574  isrim0  14577  rhmmul  14580  islring  14608  opprlring  14613  issubrng  14616  opprsubrngg  14628  issubrg  14638  resrhm2b  14666  rhmpropd  14671  rrgval  14679  aprval  14700  aprap  14707  aprprop  14710  islmod  14736  lmodprop2d  14794  islssm  14803  islssmg  14804  islssmd  14805  lssats2  14860  ellspsn  14863  ixpsnbasval  14912  islidlm  14925  isridlrng  14928  rspssp  14940  rnglidlmmgm  14942  2idlval  14948  isridl  14950  2idlelb  14951  quscrng  14979  rspsn  14980  zrhval  15061  zrhrhmb  15066  znf1o  15095  asclfval  15130  assamulgscmlem2  15151  psrgrp  15195  mplelbascoe  15208  istopon  15239  eltg  15278  eltg2  15279  eltop  15295  eltop2  15296  eltop3  15297  iscld  15329  neiss2  15368  isnei  15370  lmfval  15419  cnfval  15420  iscn  15423  iscnp  15425  tgcn  15434  tgcnp  15435  lmbrf  15441  cnptopresti  15464  txbas  15484  eltx  15485  txdis  15503  txdis1cn  15504  hmeofvalg  15529  ishmeo  15530  ispsmet  15549  ismet  15570  isxmet  15571  elblps  15616  elbl  15617  elmopn  15672  neibl  15717  metrest  15732  txmetcnp  15744  txmetcn  15745  metcnpd  15746  elcncf  15799  ellimc3apf  15886  limcmpted  15889  cnlimcim  15897  cnlimc  15898  eldvap  15908  dvidsslem  15919  dviaddf  15931  dvimulf  15932  elply  15960  ply1termlem  15968  lgseisenlem3  16396  edgval  16506  edgiedgbg  16511  edgupgren  16587  upgredg  16590  uhgr2edg  16652  umgr2edg1  16655  usgredg2vlem1  16668  usgredg2vlem2  16669  ushgredgedg  16672  ushgredgedgloop  16674  subgruhgredgdm  16716  uhgrspansubgrlem  16722  vtxdgfval  16734  vtxedgfi  16735  vtxdgop  16738  vtxdg0v  16740  vtxdeqd  16742  vtxdfifiun  16743  1loopgrvd0fi  16752  1hevtxdg0fi  16753  1hevtxdg1en  16754  wksfval  16768  iswlk  16769  wlkm  16785  uspgr2wlkeq  16811  wlkreslem  16824  wlkres  16825  istrl  16831  clwwlkg  16839  isclwwlk  16840  clwwlkccatlem  16846  isclwwlkng  16852  clwwlkn0  16854  clwwlknnn  16858  clwwlkext2edg  16868  clwwlknonmpo  16874  clwwlknon  16875  clwwlk0on0  16877  iseupth  16893  eupth2lem3lem3fi  16916  eupth2lem3lem6fi  16917  eupth2lem3lem4fi  16919  eupth2lembfi  16923  bj-sels  17145  pw1map  17230  wexmiddiffilem  17248  wexmiddifxylem  17250  nninfall  17258  nninfsellemeq  17263