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

Theorem eleq2 2494
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 2427 . . . . . 6  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
21biimpi 194 . . . . 5  |-  ( A  =  B  ->  A. x
( x  e.  A  <->  x  e.  B ) )
3219.21bi 1803 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
43anbi2d 696 . . 3  |-  ( A  =  B  ->  (
( x  =  C  /\  x  e.  A
)  <->  ( x  =  C  /\  x  e.  B ) ) )
54exbidv 1679 . 2  |-  ( A  =  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  <->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2429 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2429 . 2  |-  ( C  e.  B  <->  E. x
( x  =  C  /\  x  e.  B
) )
85, 6, 73bitr4g 288 1  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1360    = wceq 1362   E.wex 1589    e. wcel 1755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-cleq 2426  df-clel 2429
This theorem is referenced by:  eleq12  2495  eleq2i  2497  eleq2d  2500  nelneq2  2532  dvelimdc  2589  nelne1  2691  neleq2  2700  raleqf  2903  rexeqf  2904  reueq1f  2905  rmoeq1f  2906  rabeqf  2955  clel3g  3086  clel4  3088  sbcbi2  3225  sbcel2gv  3241  csbeq2  3280  difeq2  3456  uneq1  3491  ineq1  3533  unineq  3588  n0i  3630  sbnfc2  3694  disjel  3713  elif  3817  exsnrex  3902  sneqr  4028  preqr1  4034  preq12b  4036  prel12  4037  elunii  4084  eluniab  4090  ssuni  4101  elinti  4125  elintab  4127  intss1  4131  intmin  4136  intab  4146  iineq2  4176  dfiin2g  4191  breq  4282  zfrepclf  4397  axsep2  4402  zfauscl  4403  sseliALT  4411  inuni  4442  pwne0  4450  elALT  4523  rext  4528  intid  4538  opth1  4553  opthwiener  4581  ordtri1  4739  ordtri3  4742  nsuceq0  4786  suctr  4789  ordnbtwn  4796  xpeq1  4841  xpeq2  4842  opthprc  4873  funopg  5438  dffv2  5752  dffo4  5847  fnsnb  5885  elunirnALT  5957  f1oiso  6029  canth  6036  eusvobj2  6072  mpt2eq123  6134  ndmovg  6235  snnex  6371  uniuni  6374  iunpw  6379  oneqmin  6405  onuninsuci  6440  nlimsucg  6442  limomss  6470  nnlim  6478  peano5  6488  unielxp  6601  cnvf1o  6660  smoel  6807  smo11  6811  tz7.44-2  6849  oawordeulem  6981  oaordex  6985  omordi  6993  oneo  7008  oeordi  7014  oeoa  7024  oeoe  7026  nnmordi  7058  nnaordex  7065  omabs  7074  nnneo  7078  omsmolem  7080  elqsn0  7157  qsel  7167  mapsn  7242  undifixp  7287  boxriin  7293  boxcutc  7294  fineqvlem  7515  fineqv  7516  pssnn  7519  fissuni  7604  dffi2  7661  inficl  7663  dffi3  7669  wofib  7747  zfregcl  7797  en3lplem1  7808  en3lp  7810  suc11reg  7813  inf0  7815  inf3lem2  7823  inf3lem3  7824  infeq5i  7830  axinf2  7834  dfom3  7841  elom3  7842  noinfepOLD  7854  cantnfle  7867  oemapvali  7880  cantnflem1c  7883  cantnflem1  7885  cantnfleOLD  7897  cantnflem1cOLD  7906  cantnflem1OLD  7908  tc2  7950  r1sdom  7969  rankwflemb  7988  rankval3b  8021  rankunb  8045  rankuni2b  8048  tcrank  8079  cardlim  8130  cardprclem  8137  infxpenlem  8168  alephnbtwn  8229  alephordi  8232  cardaleph  8247  alephfp  8266  alephval3  8268  aceq1  8275  aceq2  8277  dfac3  8279  dfac5lem2  8282  dfac5lem4  8284  dfac2  8288  kmlem2  8308  kmlem4  8310  coflim  8418  cfsmolem  8427  fin23lem30  8499  isf32lem2  8511  isf34lem4  8534  axdc2lem  8605  axdc3lem2  8608  axdc3lem4  8610  axdc4lem  8612  zorn2lem7  8659  axdclem  8676  brdom7disj  8686  brdom6disj  8687  axpowndlem3  8752  axpowndlem3OLD  8753  winainflem  8847  iswun  8858  eltskg  8904  inar1  8929  elgrug  8946  inaprc  8990  eltskm  8997  addnidpi  9057  indpi  9063  nqereu  9085  elnp  9143  elnpi  9144  genpnnp  9161  ltaddpr  9190  dfnn2  10322  dfnn3  10323  dfuzi  10719  uz11  10870  om2uzlti  11756  axdc4uz  11788  hash2prd  12164  hashbclem  12188  hashf1lem2  12192  wrdsymb0  12242  lsw0  12250  rpnnen2lem1  13479  rpnnen2lem2  13480  sadcp1  13633  ismre  14510  isacs  14571  clatl  15268  mreclatBAD  15339  issubm  15456  cycsubg  15688  isnsg  15689  subgacs  15695  nsgacs  15696  resghm  15742  ghmeql  15748  gsmsymgreq  15916  f1otrspeq  15932  pmtrval  15936  pmtrdifellem4  15964  pmtrprfval  15972  gsumzsplit  16397  gsumzsplitOLD  16398  pgpfac1lem1  16548  pgpfac1lem5  16553  pgpfac1  16554  issubrg  16788  islss  16937  lssacs  16969  lspsneq0  17014  lmhmeql  17057  lspdisjb  17128  lidl1el  17221  lidldvgen  17258  mplcoe1  17477  mplcoe2  17480  mplcoe2OLD  17481  islindf4  18108  mdetunilem9  18267  maducoeval2  18287  madugsum  18290  istopg  18349  fiinbas  18398  topbas  18418  ppttop  18452  pptbas  18453  epttop  18454  elcls  18518  clsndisj  18520  elcls3  18528  iscldtop  18540  neiptopnei  18577  restbas  18603  restntr  18627  pnfnei  18665  mnfnei  18666  cnpimaex  18701  lmcvg  18707  iscnp4  18708  cncnpi  18723  cnconst2  18728  cnprest  18734  cnprest2  18735  cnpdis  18738  lmss  18743  lmff  18746  cnt0  18791  ist1-3  18794  cnhaus  18799  isreg2  18822  dishaus  18827  ordthauslem  18828  cmpsublem  18843  cmpsub  18844  cmpcld  18846  hauscmplem  18850  bwthOLD  18855  uncon  18874  concompid  18876  concompcon  18877  concompss  18878  1stcfb  18890  1stcrest  18898  2ndcctbss  18900  2ndcomap  18903  dis2ndc  18905  1stcelcls  18906  llyeq  18915  nllyeq  18916  restnlly  18927  restlly  18928  islly2  18929  lly1stc  18941  dislly  18942  hauspwdom  18946  llycmpkgen2  18964  txbas  18981  eltx  18982  ptpjopn  19026  ptclsg  19029  dfac14lem  19031  txcnp  19034  ptcnplem  19035  ptcnp  19036  txlly  19050  pthaus  19052  txtube  19054  txhaus  19061  txlm  19062  tx1stc  19064  txkgen  19066  xkohaus  19067  xkopt  19069  xkococnlem  19073  tgqtop  19126  kqfvima  19144  kqt0lem  19150  isr0  19151  r0cld  19152  regr1lem  19153  kqreglem1  19155  kqreglem2  19156  reghmph  19207  fbssfi  19251  isfil  19261  filuni  19299  isufil  19317  isufil2  19322  uffix  19335  fixufil  19336  uffixfr  19337  uffixsn  19339  rnelfm  19367  flimopn  19389  flimrest  19397  flimcls  19399  flftg  19410  txflf  19420  fclsopni  19429  fclsrest  19438  fclscf  19439  fcfnei  19449  alexsublem  19457  alexsubALTlem3  19462  alexsubALT  19464  tmdgsum2  19508  symgtgp  19513  subgntr  19518  opnsubg  19519  tgpconcompeqg  19523  ghmcnp  19526  tgpt0  19530  divstgpopn  19531  tsmsi  19545  tsmssubm  19557  tsmssplit  19567  isust  19619  ustn0  19636  blssps  19840  blss  19841  blssexps  19842  blssex  19843  neibl  19917  blcld  19921  metss  19924  methaus  19936  met1stc  19937  met2ndci  19938  metrest  19940  prdsxmslem2  19945  metcnp3  19956  dscopn  20007  idnghm  20163  qdensere  20190  tgioo  20214  tgqioo  20218  zdis  20234  xrge0tsms  20252  cnheibor  20368  lmmbr  20610  bcthlem4  20679  ovolicc2lem5  20845  dyadmbllem  20920  i1fd  21000  itg11  21010  itg2gt0  21079  itgeq1f  21090  bddmulibl  21157  ellimc2  21193  limcnlp  21194  ellimc3  21195  limcflf  21197  limciun  21210  lhop1lem  21326  ig1pdvds  21532  plycpn  21639  aannenlem2  21679  efopn  21987  xrlimcnp  22246  wilthlem2  22291  wilthlem3  22292  wilth  22293  tghilbert1_1  22913  tghilbert1_2  22914  colline  22917  usgra2edg  23123  usgraedg4  23127  nbgraf1olem1  23172  nbgraf1olem3  23174  nb3graprlem1  23181  nb3graprlem2  23182  uvtx01vtx  23222  uvtxnbgravtx  23225  2trllemF  23270  wlkntrl  23283  constr1trl  23309  vdgr1a  23398  vdusgra0nedg  23400  usgravd0nedg  23404  eupath2lem1  23420  lpni  23488  rngoueqz  23739  issh  24432  pjoc1  24659  h1dn0  24777  spansneleqi  24794  nonbooli  24876  pjch  24919  pjnel  24951  cdjreui  25658  rexunirn  25698  rabsnel  25710  opabdm  25766  opabrn  25767  fpwrelmapffslem  25856  fpwrelmap  25857  xrge0tsmsd  26105  tpr2rico  26195  lmxrge0  26235  indval  26323  issiga  26407  isrnsigaOLD  26408  isrnsiga  26409  ddeval1  26503  ddeval0  26504  ddemeas  26505  ismbfm  26520  isanmbfm  26524  dya2icoseg  26545  dya2iocnrect  26549  ballotlem7  26765  erdszelem1  26926  kur14lem9  26949  cnllyscon  26981  cvmcov  26999  cvmsss2  27010  cvmcov2  27011  cvmseu  27012  cvmsiota  27013  cvmopnlem  27014  cvmliftlem15  27034  rtrclreclem.trans  27194  untelirr  27205  untsucf  27207  prodeq1f  27267  dfon2lem4  27445  dfon2lem7  27448  dfon2lem9  27450  soseq  27561  frrlem4  27617  frrlem5e  27622  frrlem11  27626  nodenselem8  27675  nocvxminlem  27677  nofulllem5  27693  dfiota3  27800  funpartlem  27819  funpartfun  27820  tfrqfree  27828  linethru  28030  hilbert1.1  28031  hilbert1.2  28032  rankelg  28052  elhf2  28059  fin2so  28257  heicant  28267  mblfinlem1  28269  ftc1anc  28316  ftc2nc  28317  fneint  28390  finlocfin  28412  locfindis  28418  comppfsc  28420  neibastop2lem  28422  cover2  28448  isbnd2  28523  prdstotbnd  28534  heibor1lem  28549  grpokerinj  28591  isidl  28655  1idl  28667  0rngo  28668  ispridl  28675  smprngopr  28693  isfldidl  28709  isdmn3  28715  iuneq2f  28808  mpt2bi123f  28816  iineq12f  28818  mptbi12f  28820  elmzpcl  28904  diophren  28994  dford3lem2  29218  ttac  29227  pw2f1ocnv  29228  wepwsolem  29236  kelac1  29258  sdrgacs  29400  expgrowthi  29449  dvconstbi  29450  elunif  29580  fnchoice  29593  stoweidlem27  29665  stoweidlem35  29673  stoweidlem46  29684  stoweidlem52  29690  funressnfv  29877  fnbrafvb  29903  afvco2  29925  ndmaovg  29933  aovmpt4g  29950  fzoopth  30056  elfzonlteqm1  30068  hash2prv  30069  hashrabsn1  30076  eleclclwwlkn  30350  vdn0frgrav2  30459  vdgn0frgrav2  30460  frgrancvvdeqlem4  30469  frgrancvvdeqlem7  30472  frgrancvvdeqlemA  30473  frgrancvvdeqlemC  30475  frgrawopreg1  30486  frgrawopreg2  30487  0rng01eq  30604  ldepspr  30713  tratrb  30940  suctrALT2VD  31271  suctrALT2  31272  en3lplem1VD  31278  en3lpVD  31280  tratrbVD  31296  suctrALTcf  31357  suctrALTcfVD  31358  suctrALT3  31359  unisnALT  31361  bnj145OLD  31417  bnj216  31422  bnj563  31434  bnj956  31469  bnj545  31587  bnj548  31589  bnj570  31597  bnj900  31621  bnj929  31628  bnj964  31635  bnj983  31643  bnj1001  31650  bnj1145  31683  bnj1398  31724  bnj1498  31751  bj-rabeqd  32007  bj-cleq  32034  bj-snsetex  32036  bj-elopg  32099  lsateln0  32210  ispsubsp  32959  linepsubN  32966  elpcliN  33107  dvh3dim3N  34664  dochsnnz  34665  mapdindp3  34937
  Copyright terms: Public domain W3C validator