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

Theorem elrab 3084
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 2571 . 2  |-  F/_ x A
2 nfcv 2571 . 2  |-  F/_ x B
3 nfv 1629 . 2  |-  F/ x ps
4 elrab.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
51, 2, 3, 4elrabf 3083 1  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1652    e. wcel 1725   {crab 2701
This theorem is referenced by:  elrab3  3085  elrab2  3086  ralrab  3088  rexrab  3090  rabsnt  3873  unimax  4041  ssintub  4060  intminss  4068  reusv6OLD  4726  rabxfrd  4736  onnminsb  4776  dfom2  4839  ssnlim  4855  ssimaex  5780  weniso  6067  sorpsscmpl  6525  canth  6531  oeeulem  6836  nnawordex  6872  elpmg  7024  fineqvlem  7315  supub  7456  suplub  7457  ordtypelem6  7484  ordtypelem7  7485  hartogslem1  7503  hartogs  7505  wemapso2lem  7511  card2on  7514  elharval  7523  wdom2d  7540  cantnfs  7613  oemapvali  7632  rankuni2b  7771  scottex  7801  tskwe  7829  cardid2  7832  iscard2  7855  harval2  7876  cardmin2  7877  acni3  7920  alephsuc2  7953  kmlem1  8022  cofsmo  8141  coftr  8145  fin23lem11  8189  enfin2i  8193  fin1a2lem9  8280  fin1a2lem11  8282  axcc4  8311  axdc3lem2  8323  zorn2lem7  8374  ondomon  8430  alephval2  8439  grutsk  8689  pinq  8796  infm3  9959  infmrcl  9979  nnind  10010  peano2uz2  10349  peano5uzi  10350  dfuzi  10352  uzind  10353  uzind3  10355  uzind3OLD  10357  eluz1  10484  uzind4  10526  nnwos  10536  eqreznegel  10553  zsupss  10557  zmin  10562  elixx1  10917  elioo2  10949  elfz1  11040  flval3  11214  serge0  11369  expge0  11408  expge1  11409  hashbclem  11693  shftf  11886  rlimrege0  12365  incexc2  12610  divalglem4  12908  divalgmod  12918  bitsval  12928  bezout  13034  1nprm  13076  1idssfct  13077  isprm2  13079  phicl2  13149  hashdvds  13156  odzval  13169  odzcllem  13170  odzdvds  13173  pcpremul  13209  prmreclem1  13276  prmreclem2  13277  prmreclem3  13278  prmreclem5  13280  ramub  13373  rami  13375  ramub1lem1  13386  ramub1lem2  13387  ismre  13807  mrcflem  13823  mrcval  13827  ismri  13848  isacs  13868  isacs1i  13874  catlid  13900  catrid  13901  ismon  13951  isnat  14136  eldmcoa  14212  coaval  14215  ismhm  14732  issubm  14740  mhmeql  14756  gsumress  14769  gsumval2  14775  grplinv  14843  issubg  14936  cycsubg  14960  isnsg  14961  ghmeql  15020  isgim  15041  isga  15060  elcntz  15113  elcntzsn  15116  odid  15168  odlem2  15169  gexid  15207  gexlem2  15208  gexdvds  15210  isslw  15234  pgpssslw  15240  pj1id  15323  efgsfo  15363  oddvdssubg  15462  pgpfac1lem5  15629  ablfaclem2  15636  isirred  15796  issubrg  15860  isabv  15899  islss  16003  islmhm  16095  lmhmeql  16123  islmim  16126  islbs  16140  gsumbagdiaglem  16432  psrmulcllem  16443  psrlidm  16459  psrridm  16460  psrass1  16461  psrcom  16464  mplsubglem  16490  mpllsslem  16491  mplmonmul  16519  coe1mul2  16654  elocv  16887  isobs  16939  istopon  16982  fctop  17060  cctop  17062  ppttop  17063  pptbas  17064  epttop  17065  iscld  17083  clscld  17103  isnei  17159  neips  17169  neiptopnei  17188  iscn  17291  iscnp  17293  ordthauslem  17439  cmpsublem  17454  concompcon  17487  2ndc1stc  17506  2ndcdisj  17511  elkgen  17560  xkoopn  17613  xkoccn  17643  txdis1cn  17659  pthaus  17662  txkgen  17676  xkohaus  17677  xkococnlem  17683  xkococn  17684  xkoinjcn  17711  txcon  17713  elqtop  17721  nrmr0reg  17773  elmptrab  17851  fbssfi  17861  opnfbas  17866  elfg  17895  cfinfil  17917  csdfil  17918  supfil  17919  filssufilg  17935  uffix  17945  fixufil  17946  uffixfr  17947  uffixsn  17949  ufinffr  17953  ufilen  17954  elflim2  17988  supnfcls  18044  fclscf  18049  flimfnfcls  18052  alexsubALTlem2  18071  alexsubALTlem4  18073  alexsubALT  18074  ptcmplem2  18076  tmdgsum2  18118  symgtgp  18123  ghmcnp  18136  elutop  18255  isucn  18300  iscfilu  18310  ispsmet  18327  ismet  18345  isxmet  18346  elblps  18409  elbl  18410  restmetu  18609  icccmp  18848  elcncf  18911  ishtpy  18989  isphtpy  18998  om1elbas  19049  iscfil  19210  iscau  19221  iscmet  19229  lmle  19246  minveclem3  19322  minveclem4  19325  ovolshftlem1  19397  ovolscalem1  19401  ovolicc2lem3  19407  iundisj  19434  dyadmax  19482  dyadmbllem  19483  opnmbllem  19485  vitalilem2  19493  vitalilem3  19494  elcpn  19812  evlsval2  19933  ig1pval3  20089  coelem  20137  quotlem  20209  elqaalem1  20228  elqaalem3  20230  aannenlem1  20237  aannenlem2  20238  aalioulem2  20242  radcnv0  20324  dmarea  20788  jensen  20819  ftalem4  20850  ftalem5  20851  efnnfsumcl  20877  efchtdvds  20934  sqff1o  20957  dvdsdivcl  20958  fsumdvdsdiaglem  20960  dvdsppwf1o  20963  dvdsflf1o  20964  dvdsflsumcom  20965  musum  20968  muinv  20970  logfac2  20993  dchrelbas  21012  dchrfi  21031  lgsfle1  21081  lgsle1  21087  lgsdirprm  21105  lgsne0  21109  lgsquadlem1  21130  lgsquadlem2  21131  dchrvmasumlem1  21181  logsqvma  21228  pntleml  21297  umgrale  21348  umgra1  21353  uslgra1  21384  usgra1  21385  usgraedg2  21387  usgraedgrnv  21389  usgrarnedg  21396  usgraedg4  21398  usgraexmpl  21412  usgrares1  21416  nbgrael  21430  nbgraeledg  21434  nbgraf1olem3  21445  cusgrarn  21460  nbcusgra  21464  cusgrares  21473  uvtxel  21490  uvtxnbgra  21494  cusgrauvtxb  21497  eupath2  21694  umgrabi  21697  konigsberg  21701  grpoidinv2  21798  grpoinv  21807  isssp  22215  islno  22246  isblo  22275  ishmo  22304  ubthlem1  22364  ubthlem2  22365  htthlem  22412  ocel  22775  shsval2i  22881  ococin  22902  chsupsn  22907  eleigvec  23452  cnlnadjlem5  23566  shatomistici  23856  hatomistici  23857  indf1ofs  24415  sigagenval  24515  ismbfm  24594  imambfm  24604  dya2iocuni  24625  issibf  24640  sitgfval  24647  dstfrvel  24723  ballotlemfc0  24742  ballotlemfcc  24743  ballotlemiex  24751  ballotlemfrcn0  24779  ballotlemirc  24781  ballotlem7  24785  conpcon  24914  iscvm  24938  cvmsi  24944  cvmsval  24945  cvmliftmolem2  24961  cvmliftiota  24980  snmlval  25010  elgiso  25099  sltval2  25603  sltres  25611  nodenselem7  25634  nofulllem5  25653  lineelsb2  26074  linerflx1  26075  rankeq1o  26104  mblfinlem  26234  itg2gt0cn  26250  finminlem  26312  fneint  26348  fnessref  26364  locfincmp  26375  topmeet  26384  topjoin  26385  neifg  26391  indexa  26426  nninfnub  26446  istotbnd  26469  sstotbnd2  26474  isbnd  26480  isrngohom  26572  isrngoiso  26585  isidl  26615  ispridl  26635  ismaxidl  26641  prnc  26668  isfldidl  26669  isnacs  26749  elmzpcl  26774  mzpindd  26794  rencldnfilem  26872  irrapxlem6  26881  pellexlem3  26885  pellexlem5  26887  elpell1qr  26901  elpell14qr  26903  elpell1234qr  26905  pellfundre  26935  pellfundge  26936  pellfundlb  26938  pellfundglb  26939  rmspecnonsq  26961  jm2.22  27057  jm2.23  27058  rpnnen3lem  27093  fnwe2lem2  27117  fnwe2lem3  27118  dsmmelbas  27173  frlmelbas  27192  frlmssuvc2  27215  islinds  27247  elmnc  27309  dgraalem  27318  dgraaub  27321  mpaalem  27325  rgspnmin  27344  issubmd  27351  pmtrval  27362  pmtrrn  27367  symgsssg  27376  symgfisg  27377  psgnunilem5  27385  issdrg  27473  phisum  27486  stoweidlem14  27730  stoweidlem15  27731  stoweidlem16  27732  stoweidlem31  27747  stoweidlem36  27752  stoweidlem46  27762  stoweidlem48  27764  el2wlkonot  28289  el2spthonot  28290  el2spthonot0  28291  el2wlksoton  28298  el2spthsoton  28299  el2wlksotot  28302  2spotdisj  28387  usg2spot2nb  28391  usgreg2spot  28393  secval  28427  cscval  28428  cotval  28429  islshp  29714  lssats  29747  islfl  29795  isat  30021  atlatmstc  30054  islln  30240  islpln  30264  islvol  30307  linepsubN  30486  elpmap  30492  pmapsub  30502  elpadd  30533  paddvaln0N  30535  islhp  30730  isldil  30844  isltrn  30853  isdilN  30888  istrnN  30891  diaval  31767  diaelval  31768  diaeldm  31771  diaelrnN  31780  cdlemm10N  31853  docaclN  31859  dibglbN  31901  dicval  31911  dicfnN  31918  dicvalrelN  31920  dihglblem2aN  32028  dihglblem2N  32029  dihglblem3N  32030  dih1dimatlem  32064  dihglb2  32077  dochvalr  32092  doch2val2  32099  dochocss  32101  islpolN  32218  mapd0  32400
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-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950
  Copyright terms: Public domain W3C validator