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  7319  ordiso2  7376  ctssdccl  7452  nnnninfeq  7469  cc2lem  7633  cc2  7634  cc3  7635  archnqq  7785  ltdfpr  7874  genpelxp  7879  genpelvl  7880  genpelvu  7881  addcanprleml  7982  addcanprlemu  7983  cauappcvgprlem1  8027  suplocexprlemell  8081  suplocexprlemmu  8086  suplocexprlemru  8087  suplocexprlemdisj  8088  suplocexprlemloc  8089  suplocexprlemub  8091  suplocexprlemlub  8092  cnm  8200  indval0  9300  eluz1  9935  elixx1  10310  elioo2  10334  elfz1  10427  elfzp1  10490  fzpr  10495  fzsuc2  10497  fzrev3  10505  elfzp12  10517  fzm1  10518  fzoval  10566  elfzo  10567  fzodcel  10571  elfzom1b  10658  fzosplitsni  10665  nninfdcex  10683  zmodidfzo  10805  frecuzrdgtcl  10864  frecuzrdgfunlem  10871  seqf1og  10973  bcval  11203  bcpasc  11220  hashf1lem1  11301  fundm2domnop0  11316  wrdmap  11352  elovmpowrd  11362  ccatfvalfi  11376  elfzelfzccat  11384  ccatlid  11390  ccatass  11392  ccatrn  11393  ccatalpha  11397  swrdfv2  11451  ccatswrd  11458  swrdccat2  11459  pfxfv  11472  pfxeq  11484  ccatpfx  11489  swrdswrd  11493  swrdpfx  11495  pfxpfx  11496  cats1un  11509  swrdccatfn  11512  swrdccatin1  11513  pfxccatin12lem4  11514  pfxccatin12lem1  11516  swrdccatin2  11517  pfxccatin12lem2c  11518  pfxccatin12lem2  11519  swrdccat3blem  11527  swrdccatin1d  11531  swrdccatin2d  11532  pfxccatin12d  11533  shftfn  11605  shftval  11606  seq3shft  11619  iser3shft  12131  sumeq1  12140  summodclem3  12166  summodclem2a  12167  isumss  12177  fsumsplit  12193  sumsplitdc  12218  fsum2dlemstep  12220  fisumcom2  12224  fsumparts  12256  explecnv  12291  fprodsplitdc  12382  fprodsplit  12383  fprod2dlemstep  12408  fprodcom2fi  12412  eftlub  12476  divalgmod  12713  bitsval  12729  bitsp1e  12738  bitsp1o  12739  algfx  12849  eucalgcvga  12855  reumodprminv  13055  nnnn0modprm0  13057  prmlem0  13243  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemsima  13311  ballotfilemrv  13315  ennnfonelemex  13357  ennnfonelemhom  13358  ennnfonelemf1  13361  ennnfonelemrn  13362  ctinfomlemom  13370  ctinfom  13371  ctiunctlemudc  13380  ctiunctlemf  13381  elrest  13653  ptex  13671  imasaddfnlemg  13688  divsfval  13702  xpscf  13721  grpidvalg  13746  grpidpropdg  13747  grpidd  13756  issgrpd  13780  sgrppropd  13781  ismndd  13803  mndpropd  13806  imasmnd2  13812  imasmnd  13813  ismhm  13821  issubm  13832  imasgrp2  13966  imasgrp  13967  issubg  14029  subginv  14037  isnsg  14058  eqg0el  14085  quselbasg  14086  isghm  14099  resghm2b  14118  conjnmzb  14136  conjnsg  14137  ghmpropd  14139  cntrval  14145  cntzval  14147  elcntz  14148  elcntzsn  14151  resscntz  14160  imasabl  14224  gzsumsplit0  14232  gsummptfidmsplit  14248  prdsbasmpt  14271  prdsbasmpt2  14279  pwselbasb  14297  mgpplusg  14313  mgpbas  14316  isrngd  14343  rngpropd  14345  imasrng  14346  qusrng  14348  rng1zrlem  14349  ringidval  14356  dfur2g  14357  srgidmlem  14373  issrgid  14376  ringcl  14408  isringid  14421  isringd  14437  imasring  14460  oppr0g  14478  oppr1g  14479  dvdsrvald  14491  isunitd  14504  unitinvcl  14521  unitinvinv  14522  unitlinv  14524  unitrinv  14525  unitnegcl  14528  dvdsrpropdg  14545  isrhm  14556  isrim0  14559  rhmmul  14562  islring  14590  opprlring  14595  issubrng  14598  opprsubrngg  14610  issubrg  14620  resrhm2b  14648  rhmpropd  14653  rrgval  14661  aprval  14682  aprap  14689  aprprop  14692  islmod  14718  lmodprop2d  14776  islssm  14785  islssmg  14786  islssmd  14787  lssats2  14842  ellspsn  14845  ixpsnbasval  14894  islidlm  14907  isridlrng  14910  rspssp  14922  rnglidlmmgm  14924  2idlval  14930  isridl  14932  2idlelb  14933  quscrng  14961  rspsn  14962  zrhval  15043  zrhrhmb  15048  znf1o  15077  asclfval  15112  assamulgscmlem2  15133  psrgrp  15174  mplelbascoe  15182  istopon  15213  eltg  15252  eltg2  15253  eltop  15269  eltop2  15270  eltop3  15271  iscld  15303  neiss2  15342  isnei  15344  lmfval  15393  cnfval  15394  iscn  15397  iscnp  15399  tgcn  15408  tgcnp  15409  lmbrf  15415  cnptopresti  15438  txbas  15458  eltx  15459  txdis  15477  txdis1cn  15478  hmeofvalg  15503  ishmeo  15504  ispsmet  15523  ismet  15544  isxmet  15545  elblps  15590  elbl  15591  elmopn  15646  neibl  15691  metrest  15706  txmetcnp  15718  txmetcn  15719  metcnpd  15720  elcncf  15773  ellimc3apf  15860  limcmpted  15863  cnlimcim  15871  cnlimc  15872  eldvap  15882  dvidsslem  15893  dviaddf  15905  dvimulf  15906  elply  15934  ply1termlem  15942  lgseisenlem3  16370  edgval  16480  edgiedgbg  16485  edgupgren  16561  upgredg  16564  uhgr2edg  16626  umgr2edg1  16629  usgredg2vlem1  16642  usgredg2vlem2  16643  ushgredgedg  16646  ushgredgedgloop  16648  subgruhgredgdm  16690  uhgrspansubgrlem  16696  vtxdgfval  16708  vtxedgfi  16709  vtxdgop  16712  vtxdg0v  16714  vtxdeqd  16716  vtxdfifiun  16717  1loopgrvd0fi  16726  1hevtxdg0fi  16727  1hevtxdg1en  16728  wksfval  16742  iswlk  16743  wlkm  16759  uspgr2wlkeq  16785  wlkreslem  16798  wlkres  16799  istrl  16805  clwwlkg  16813  isclwwlk  16814  clwwlkccatlem  16820  isclwwlkng  16826  clwwlkn0  16828  clwwlknnn  16832  clwwlkext2edg  16842  clwwlknonmpo  16848  clwwlknon  16849  clwwlk0on0  16851  iseupth  16867  eupth2lem3lem3fi  16890  eupth2lem3lem6fi  16891  eupth2lem3lem4fi  16893  eupth2lembfi  16897  bj-sels  17119  pw1map  17204  wexmiddiffilem  17222  wexmiddifxylem  17224  nninfall  17231  nninfsellemeq  17236