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

Theorem elrab 3106
Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.)
Hypothesis
Ref Expression
elrab.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
elrab  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
Distinct variable groups:    ps, x    x, A    x, B
Allowed substitution hint:    ph( x)

Proof of Theorem elrab
StepHypRef Expression
1 nfcv 2569 . 2  |-  F/_ x A
2 nfcv 2569 . 2  |-  F/_ x B
3 nfv 1672 . 2  |-  F/ x ps
4 elrab.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
51, 2, 3, 4elrabf 3104 1  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1362    e. wcel 1755   {crab 2709
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-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964
This theorem is referenced by:  elrab3  3107  elrab2  3108  ralrab  3110  rexrab  3112  rabsnt  3940  unimax  4115  ssintub  4134  intminss  4142  reusv6OLD  4491  rabxfrd  4501  ssimaex  5744  weniso  6032  canth  6036  sorpsscmpl  6360  onnminsb  6404  dfom2  6467  ssnlim  6483  elsuppfn  6687  ressuppssdif  6699  oeeulem  7028  nnawordex  7064  elpmg  7216  fineqvlem  7515  mapfienlem2  7643  supub  7697  suplub  7698  ordtypelem6  7725  ordtypelem7  7726  hartogslem1  7744  hartogs  7746  wemapsolem  7752  card2on  7757  elharval  7766  wdom2d  7783  cantnfs  7862  oemapvali  7880  cantnfsOLD  7892  rankuni2b  8048  scottex  8080  tskwe  8108  cardid2  8111  iscard2  8134  harval2  8155  cardmin2  8156  acni3  8205  alephsuc2  8238  kmlem1  8307  cofsmo  8426  coftr  8430  fin23lem11  8474  enfin2i  8478  fin1a2lem9  8565  fin1a2lem11  8567  axcc4  8596  axdc3lem2  8608  zorn2lem7  8659  ondomon  8715  alephval2  8724  grutsk  8977  pinq  9084  infm3  10277  infmrcl  10297  nnind  10328  peano2uz2  10717  peano5uzi  10718  dfuzi  10720  uzind  10721  uzind3  10723  uzind3OLD  10725  eluz1  10853  uzind4  10900  nnwos  10910  eqreznegel  10928  zsupss  10932  zmin  10937  elixx1  11297  elioo2  11329  elfz1  11429  flval3  11647  serge0  11844  expge0  11884  expge1  11885  pr2pwpr  12167  hashbclem  12189  disjxwrd  12333  shftf  12552  rlimrege0  13041  incexc2  13284  divalglem4  13583  divalgmod  13593  bitsval  13603  bezout  13709  1nprm  13751  1idssfct  13752  isprm2  13754  phicl2  13826  hashdvds  13833  odzval  13846  odzcllem  13847  odzdvds  13850  pcpremul  13893  prmreclem1  13960  prmreclem2  13961  prmreclem3  13962  prmreclem5  13964  ramub  14057  rami  14059  ramub1lem1  14070  ramub1lem2  14071  ismre  14511  mrcflem  14527  mrcval  14531  ismri  14552  isacs  14572  isacs1i  14578  catlid  14604  catrid  14605  ismon  14655  isnat  14840  eldmcoa  14916  coaval  14919  lubeldm  15134  glbeldm  15147  ismhm  15449  issubm  15457  issubmd  15459  mhmeql  15474  mrcmndind  15476  gsumress  15487  gsumval2  15493  grplinv  15564  issubg  15661  cycsubg  15689  isnsg  15690  ghmeql  15749  isgim  15770  isga  15789  elcntz  15820  elcntzsn  15823  symgfix2  15901  pmtrval  15937  pmtrrn  15943  symgsssg  15953  symgfisg  15954  psgnunilem5  15980  odid  16021  odlem2  16022  gexid  16060  gexlem2  16061  gexdvds  16063  isslw  16087  pgpssslw  16093  pj1id  16176  efgsfo  16216  oddvdssubg  16317  pgpfac1lem5  16554  ablfaclem2  16561  isirred  16725  issubrg  16789  isabv  16828  islss  16938  islmhm  17030  lmhmeql  17058  islmim  17065  islbs  17079  gsumbagdiaglem  17379  psrmulcllem  17392  psrlidm  17408  psrlidmOLD  17409  psrridm  17410  psrridmOLD  17411  psrass1  17412  psrcom  17415  mplsubglem  17444  mpllsslem  17445  mplsubglemOLD  17446  mpllsslemOLD  17447  mplmonmul  17477  coe1mul2  17621  zrhcofipsgn  17865  psgndiflemB  17872  elocv  17935  isobs  17987  dsmmelbas  18006  frlmelbas  18024  frlmelbasOLD  18025  frlmssuvc2  18062  frlmssuvc2OLD  18064  islinds  18080  symgmatr01lem  18301  istopon  18372  fctop  18450  cctop  18452  ppttop  18453  pptbas  18454  epttop  18455  iscld  18473  clscld  18493  isnei  18549  neips  18559  neiptopnei  18578  iscn  18681  iscnp  18683  ordthauslem  18829  cmpsublem  18844  concompcon  18878  2ndc1stc  18897  2ndcdisj  18902  elkgen  18951  xkoopn  19004  xkoccn  19034  txdis1cn  19050  pthaus  19053  txkgen  19067  xkohaus  19068  xkococnlem  19074  xkococn  19075  xkoinjcn  19102  txcon  19104  elqtop  19112  nrmr0reg  19164  elmptrab  19242  fbssfi  19252  opnfbas  19257  elfg  19286  cfinfil  19308  csdfil  19309  supfil  19310  filssufilg  19326  uffix  19336  fixufil  19337  uffixfr  19338  uffixsn  19340  ufinffr  19344  ufilen  19345  elflim2  19379  supnfcls  19435  fclscf  19440  flimfnfcls  19443  alexsubALTlem2  19462  alexsubALTlem4  19464  alexsubALT  19465  ptcmplem2  19467  tmdgsum2  19509  symgtgp  19514  ghmcnp  19527  elutop  19650  isucn  19695  iscfilu  19705  ispsmet  19722  ismet  19740  isxmet  19741  elblps  19804  elbl  19805  restmetu  20004  icccmp  20244  elcncf  20307  ishtpy  20386  isphtpy  20395  om1elbas  20446  iscfil  20618  iscau  20629  iscmet  20637  lmle  20654  rrxfsupp  20743  minveclem3  20758  minveclem4  20761  ovolshftlem1  20834  ovolscalem1  20838  ovolicc2lem3  20844  iundisj  20871  dyadmax  20920  dyadmbllem  20921  opnmbllem  20923  vitalilem2  20931  vitalilem3  20932  elcpn  21250  evlsval2  21372  ig1pval3  21531  coelem  21579  quotlem  21651  elqaalem1  21670  elqaalem3  21672  aannenlem1  21679  aannenlem2  21680  aalioulem2  21684  radcnv0  21766  dmarea  22236  jensen  22267  ftalem4  22298  ftalem5  22299  efnnfsumcl  22325  efchtdvds  22382  sqff1o  22405  dvdsdivcl  22406  fsumdvdsdiaglem  22408  dvdsppwf1o  22411  dvdsflf1o  22412  dvdsflsumcom  22413  musum  22416  muinv  22418  logfac2  22441  dchrelbas  22460  dchrfi  22479  lgsfle1  22529  lgsle1  22535  lgsdirprm  22553  lgsne0  22557  lgsquadlem1  22578  lgsquadlem2  22579  dchrvmasumlem1  22629  logsqvma  22676  pntleml  22745  tgellng  22866  mircgr  22927  mirbtwn  22928  ttgelitv  22952  ebtwntg  23051  umgrale  23078  umgra1  23083  uslgra1  23114  usgra1  23115  usgraedg2  23117  usgraedgrnv  23119  usgrarnedg  23126  usgraedg4  23128  usgraexmpl  23142  usgrares1  23146  nbgrael  23160  nbgraeledg  23164  nbgraf1olem3  23175  cusgrarn  23190  nbcusgra  23194  cusgrares  23203  uvtxel  23220  uvtxnbgra  23224  cusgrauvtxb  23227  eupath2  23424  umgrabi  23427  konigsberg  23431  grpoidinv2  23528  grpoinv  23537  isssp  23945  islno  23976  isblo  24005  ishmo  24034  ubthlem1  24094  ubthlem2  24095  htthlem  24142  ocel  24507  shsval2i  24613  ococin  24634  chsupsn  24639  eleigvec  25184  cnlnadjlem5  25298  shatomistici  25588  hatomistici  25589  nnindf  25912  ordtconlem1  26208  indf1ofs  26336  sigagenval  26437  ddemeas  26506  ismbfm  26521  imambfm  26531  dya2iocuni  26552  issibf  26567  sitgfval  26575  oddpwdc  26585  eulerpartlemgh  26609  eulerpartlemgs2  26611  dstfrvel  26704  ballotlemfc0  26723  ballotlemfcc  26724  ballotlemiex  26732  ballotlemfrcn0  26760  ballotlemirc  26762  ballotlem7  26766  conpcon  26972  iscvm  26996  cvmsi  27002  cvmsval  27003  cvmliftmolem2  27019  cvmliftiota  27038  snmlval  27068  elgiso  27162  sltval2  27644  sltres  27652  nodenselem7  27675  nofulllem5  27694  lineelsb2  28026  linerflx1  28027  rankeq1o  28056  fin2solem  28259  fin2so  28260  opnmbllem0  28271  mblfinlem2  28273  itg2gt0cn  28291  finminlem  28357  fneint  28393  fnessref  28409  locfincmp  28420  topmeet  28429  topjoin  28430  neifg  28436  indexa  28471  nninfnub  28491  istotbnd  28512  sstotbnd2  28517  isbnd  28523  isrngohom  28615  isrngoiso  28628  isidl  28658  ispridl  28678  ismaxidl  28684  prnc  28711  isfldidl  28712  isnacs  28885  elmzpcl  28907  mzpindd  28927  rencldnfilem  29004  irrapxlem6  29013  pellexlem3  29017  pellexlem5  29019  elpell1qr  29033  elpell14qr  29035  elpell1234qr  29037  pellfundre  29067  pellfundge  29068  pellfundlb  29070  pellfundglb  29071  rmspecnonsq  29093  jm2.22  29189  jm2.23  29190  rpnnen3lem  29225  fnwe2lem2  29249  fnwe2lem3  29250  elmnc  29338  dgraalem  29347  dgraaub  29350  mpaalem  29354  rgspnmin  29373  issdrg  29399  phisum  29412  stoweidlem14  29655  stoweidlem15  29656  stoweidlem16  29657  stoweidlem31  29672  stoweidlem36  29677  stoweidlem46  29687  stoweidlem48  29689  elss2pr  30074  wwlktovf  30097  wwlktovf1  30098  wwlktovfo  30099  iswwlk  30163  iswwlkn  30164  wlknwwlknsur  30190  wlkiswwlksur  30197  wwlkextinj  30208  wwlkextsur  30209  wlknwwlknvbij  30218  el2wlkonot  30234  el2spthonot  30235  el2spthonot0  30236  el2wlksoton  30243  el2spthsoton  30244  el2wlksotot  30247  isclwwlk  30277  isclwwlkn  30278  clwwlkprop  30279  clwwlknprop  30281  clwwlkvbij  30309  Lemma2  30339  eleclclwwlkn  30353  clwlkfclwwlk1hashn  30360  clwlkf1clwwlklem1  30365  clwlkf1clwwlklem2  30366  rusgranumwlklem0  30412  rusgranumwlklem1  30413  rusgranumwlklem3  30415  rusgranumwlks  30420  2spotdisj  30500  usg2spot2nb  30504  usgreg2spot  30506  numclwwlkun  30518  numclwwlkovfel2  30522  numclwwlkovgel  30527  numclwlk1lem2foa  30530  numclwwlk2lem1  30541  numclwlk2lem2f  30542  numclwlk2lem2f1o  30544  lcoval  30655  secval  30791  cscval  30792  cotval  30793  islshp  32197  lssats  32230  islfl  32278  isat  32504  atlatmstc  32537  islln  32723  islpln  32747  islvol  32790  linepsubN  32969  elpmap  32975  pmapsub  32985  elpadd  33016  paddvaln0N  33018  islhp  33213  isldil  33327  isltrn  33336  isdilN  33371  istrnN  33374  diaval  34250  diaelval  34251  diaeldm  34254  diaelrnN  34263  cdlemm10N  34336  docaclN  34342  dibglbN  34384  dicval  34394  dicfnN  34401  dicvalrelN  34403  dihglblem2aN  34511  dihglblem2N  34512  dihglblem3N  34513  dih1dimatlem  34547  dihglb2  34560  dochvalr  34575  doch2val2  34582  dochocss  34584  islpolN  34701  mapd0  34883
  Copyright terms: Public domain W3C validator