MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eleq2 Structured version   Unicode version

Theorem eleq2 2497
Description: Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
eleq2  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )

Proof of Theorem eleq2
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 dfcleq 2430 . . . . . 6  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
21biimpi 187 . . . . 5  |-  ( A  =  B  ->  A. x
( x  e.  A  <->  x  e.  B ) )
3219.21bi 1774 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
43anbi2d 685 . . 3  |-  ( A  =  B  ->  (
( x  =  C  /\  x  e.  A
)  <->  ( x  =  C  /\  x  e.  B ) ) )
54exbidv 1636 . 2  |-  ( A  =  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  <->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2432 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2432 . 2  |-  ( C  e.  B  <->  E. x
( x  =  C  /\  x  e.  B
) )
85, 6, 73bitr4g 280 1  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1549   E.wex 1550    = wceq 1652    e. wcel 1725
This theorem is referenced by:  eleq12  2498  eleq2i  2500  eleq2d  2503  nelneq2  2535  dvelimdc  2592  nelne1  2693  neleq2  2700  raleqf  2900  rexeqf  2901  reueq1f  2902  rmoeq1f  2903  rabeqf  2949  clel3g  3073  clel4  3075  sbcel2gv  3221  sbnfc2  3309  difeq2  3459  uneq1  3494  ineq1  3535  unineq  3591  n0i  3633  disjel  3674  elif  3773  exsnrex  3848  sneqr  3966  preqr1  3972  preq12b  3974  prel12  3975  elunii  4020  eluniab  4027  ssuni  4037  elinti  4059  elintab  4061  intss1  4065  intmin  4070  intab  4080  iineq2  4110  dfiin2g  4124  breq  4214  zfrepclf  4326  axsep2  4331  zfauscl  4332  inuni  4362  elALT  4407  rext  4412  intid  4421  opth1  4434  opthwiener  4458  ordtri1  4614  ordtri3  4617  nsuceq0  4661  suctrALT  4664  ordnbtwn  4672  snnex  4713  uniuni  4716  iunpw  4759  oneqmin  4785  onuninsuci  4820  nlimsucg  4822  limomss  4850  nnlim  4858  peano5  4868  xpeq1  4892  xpeq2  4893  opthprc  4925  funopg  5485  dffv2  5796  dffo4  5885  elunirnALT  6000  f1oiso  6071  mpt2eq123  6133  ndmovg  6230  unielxp  6385  cnvf1o  6445  canth  6539  eusvobj2  6582  smoel  6622  smo11  6626  tz7.44-2  6665  oawordeulem  6797  oaordex  6801  omordi  6809  oneo  6824  oeordi  6830  oeoa  6840  oeoe  6842  nnmordi  6874  nnaordex  6881  omabs  6890  nnneo  6894  omsmolem  6896  elqsn0  6973  qsel  6983  mapsn  7055  undifixp  7098  boxriin  7104  boxcutc  7105  fineqvlem  7323  fineqv  7324  pssnn  7327  fissuni  7411  dffi2  7428  inficl  7430  dffi3  7436  wofib  7514  zfregcl  7562  suc11reg  7574  inf0  7576  inf3lem2  7584  inf3lem3  7585  infeq5i  7591  axinf2  7595  dfom3  7602  elom3  7603  noinfepOLD  7615  cantnfle  7626  oemapvali  7640  cantnflem1c  7643  cantnflem1  7645  en3lplem1  7670  en3lp  7672  tc2  7681  r1sdom  7700  rankwflemb  7719  rankval3b  7752  rankunb  7776  rankuni2b  7779  tcrank  7808  cardlim  7859  cardprclem  7866  infxpenlem  7895  alephnbtwn  7952  alephordi  7955  cardaleph  7970  alephfp  7989  alephval3  7991  aceq1  7998  aceq2  8000  dfac3  8002  dfac5lem2  8005  dfac5lem4  8007  dfac2  8011  kmlem2  8031  kmlem4  8033  coflim  8141  cfsmolem  8150  fin23lem30  8222  isf32lem2  8234  isf34lem4  8257  axdc2lem  8328  axdc3lem2  8331  axdc3lem4  8333  axdc4lem  8335  zorn2lem7  8382  axdclem  8399  brdom7disj  8409  brdom6disj  8410  axpowndlem3  8474  winainflem  8568  iswun  8579  eltskg  8625  inar1  8650  elgrug  8667  inaprc  8711  eltskm  8718  addnidpi  8778  indpi  8784  nqereu  8806  elnp  8864  elnpi  8865  genpnnp  8882  ltaddpr  8911  dfnn2  10013  dfnn3  10014  dfuzi  10360  uz11  10508  om2uzlti  11290  axdc4uz  11322  hashbclem  11701  hashf1lem2  11705  rpnnen2lem1  12814  rpnnen2lem2  12815  sadcp1  12967  ismre  13815  isacs  13876  mreclat  14613  issubm  14748  cycsubg  14968  isnsg  14969  subgacs  14975  nsgacs  14976  resghm  15022  ghmeql  15028  gsumzsplit  15529  pgpfac1lem1  15632  pgpfac1lem5  15637  pgpfac1  15638  issubrg  15868  islss  16011  lssacs  16043  lspsneq0  16088  lmhmeql  16131  lspdisjb  16198  lidl1el  16289  lidldvgen  16326  mplcoe1  16528  mplcoe2  16530  istopg  16968  fiinbas  17017  topbas  17037  ppttop  17071  pptbas  17072  epttop  17073  elcls  17137  clsndisj  17139  elcls3  17147  iscldtop  17159  neiptopnei  17196  restbas  17222  restntr  17246  pnfnei  17284  mnfnei  17285  cnpimaex  17320  lmcvg  17326  iscnp4  17327  cncnpi  17342  cnconst2  17347  cnprest  17353  cnprest2  17354  cnpdis  17357  lmss  17362  lmff  17365  cnt0  17410  ist1-3  17413  cnhaus  17418  isreg2  17441  dishaus  17446  ordthauslem  17447  cmpsublem  17462  cmpsub  17463  cmpcld  17465  hauscmplem  17469  bwth  17473  uncon  17492  concompid  17494  concompcon  17495  concompss  17496  1stcfb  17508  1stcrest  17516  2ndcctbss  17518  2ndcomap  17521  dis2ndc  17523  1stcelcls  17524  llyeq  17533  nllyeq  17534  restnlly  17545  restlly  17546  islly2  17547  lly1stc  17559  dislly  17560  hauspwdom  17564  llycmpkgen2  17582  txbas  17599  eltx  17600  ptpjopn  17644  ptclsg  17647  dfac14lem  17649  txcnp  17652  ptcnplem  17653  ptcnp  17654  txlly  17668  pthaus  17670  txtube  17672  txhaus  17679  txlm  17680  tx1stc  17682  txkgen  17684  xkohaus  17685  xkopt  17687  xkococnlem  17691  tgqtop  17744  kqfvima  17762  kqt0lem  17768  isr0  17769  r0cld  17770  regr1lem  17771  kqreglem1  17773  kqreglem2  17774  reghmph  17825  fbssfi  17869  isfil  17879  filuni  17917  isufil  17935  isufil2  17940  uffix  17953  fixufil  17954  uffixfr  17955  uffixsn  17957  rnelfm  17985  flimopn  18007  flimrest  18015  flimcls  18017  flftg  18028  txflf  18038  fclsopni  18047  fclsrest  18056  fclscf  18057  fcfnei  18067  alexsublem  18075  alexsubALTlem3  18080  alexsubALT  18082  tmdgsum2  18126  symgtgp  18131  subgntr  18136  opnsubg  18137  tgpconcompeqg  18141  ghmcnp  18144  tgpt0  18148  divstgpopn  18149  tsmsi  18163  tsmssubm  18172  tsmssplit  18181  isust  18233  ustn0  18250  blssps  18454  blss  18455  blssexps  18456  blssex  18457  neibl  18531  blcld  18535  metss  18538  methaus  18550  met1stc  18551  met2ndci  18552  metrest  18554  prdsxmslem2  18559  metcnp3  18570  dscopn  18621  idnghm  18777  qdensere  18804  tgioo  18827  tgqioo  18831  zdis  18847  xrge0tsms  18865  cnheibor  18980  lmmbr  19211  bcthlem4  19280  ovolicc2lem5  19417  dyadmbllem  19491  i1fd  19573  itg11  19583  itg2gt0  19652  itgeq1f  19663  bddmulibl  19730  ellimc2  19764  limcnlp  19765  ellimc3  19766  limcflf  19768  limciun  19781  lhop1lem  19897  ig1pdvds  20099  plycpn  20206  aannenlem2  20246  efopn  20549  xrlimcnp  20807  wilthlem2  20852  wilthlem3  20853  wilth  20854  usgra2edg  21402  usgraedg4  21406  nbgraf1olem1  21451  nbgraf1olem3  21453  nb3graprlem1  21460  nb3graprlem2  21461  uvtx01vtx  21501  uvtxnbgravtx  21504  2trllemF  21549  wlkntrl  21562  constr1trl  21588  vdgr1a  21677  vdusgra0nedg  21679  usgravd0nedg  21683  eupath2lem1  21699  lpni  21767  rngoueqz  22018  issh  22710  pjoc1  22936  h1dn0  23054  spansneleqi  23071  nonbooli  23153  pjch  23196  pjnel  23228  cdjreui  23935  rexunirn  23978  xrge0tsmsd  24223  tpr2rico  24310  lmxrge0  24337  indval  24411  issiga  24494  isrnsigaOLD  24495  isrnsiga  24496  ismbfm  24602  isanmbfm  24606  dya2icoseg  24627  dya2iocnrect  24631  ballotlem7  24793  erdszelem1  24877  kur14lem9  24900  cnllyscon  24932  cvmcov  24950  cvmsss2  24961  cvmcov2  24962  cvmseu  24963  cvmsiota  24964  cvmopnlem  24965  cvmliftlem15  24985  rtrclreclem.trans  25146  untelirr  25157  untsucf  25159  prodeq1f  25234  dfon2lem4  25413  dfon2lem7  25416  dfon2lem9  25418  soseq  25529  frrlem4  25585  frrlem5e  25590  frrlem11  25594  nodenselem8  25643  nocvxminlem  25645  nofulllem5  25661  dfiota3  25768  funpartlem  25787  funpartfun  25788  tfrqfree  25796  linethru  26087  hilbert1.1  26088  hilbert1.2  26089  rankelg  26109  elhf2  26116  mblfinlem1  26243  ftc1anc  26288  ftc2nc  26289  fneint  26357  finlocfin  26379  locfindis  26385  comppfsc  26387  neibastop2lem  26389  cover2  26415  isbnd2  26492  prdstotbnd  26503  heibor1lem  26518  grpokerinj  26560  isidl  26624  1idl  26636  0rngo  26637  ispridl  26644  smprngopr  26662  isfldidl  26678  isdmn3  26684  elmzpcl  26783  diophren  26874  dford3lem2  27098  ttac  27107  pw2f1ocnv  27108  wepwsolem  27116  kelac1  27138  f1otrspeq  27367  pmtrval  27371  sdrgacs  27486  expgrowthi  27527  dvconstbi  27528  elunif  27663  fnchoice  27676  stoweidlem27  27752  stoweidlem35  27760  stoweidlem46  27771  stoweidlem52  27777  funressnfv  27968  fnbrafvb  27994  afvco2  28016  ndmaovg  28024  aovmpt4g  28041  fzoopth  28139  wrdsymb0  28170  lswrd0  28261  vdn0frgrav2  28414  vdgn0frgrav2  28415  frgrancvvdeqlem4  28422  frgrancvvdeqlem7  28425  frgrancvvdeqlemA  28426  frgrancvvdeqlemC  28428  frgrawopreg1  28439  frgrawopreg2  28440  tratrb  28620  suctrALT2VD  28948  suctrALT2  28949  en3lplem1VD  28955  en3lpVD  28957  tratrbVD  28973  suctrALTcf  29034  suctrALTcfVD  29035  suctrALT3  29036  unisnALT  29038  bnj145  29094  bnj216  29099  bnj563  29111  bnj956  29147  bnj545  29266  bnj548  29268  bnj570  29276  bnj900  29300  bnj929  29307  bnj964  29314  bnj983  29322  bnj1001  29329  bnj1145  29362  bnj1398  29403  bnj1498  29430  lsateln0  29793  ispsubsp  30542  linepsubN  30549  elpcliN  30690  dvh3dim3N  32247  dochsnnz  32248  mapdindp3  32520
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2429  df-clel 2432
  Copyright terms: Public domain W3C validator