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

Theorem elrab 3036
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 2524 . 2  |-  F/_ x A
2 nfcv 2524 . 2  |-  F/_ x B
3 nfv 1626 . 2  |-  F/ x ps
4 elrab.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
51, 2, 3, 4elrabf 3035 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 1649    e. wcel 1717   {crab 2654
This theorem is referenced by:  elrab3  3037  elrab2  3038  ralrab  3040  rexrab  3042  rabsnt  3825  unimax  3992  ssintub  4011  intminss  4019  reusv6OLD  4675  rabxfrd  4685  onnminsb  4725  dfom2  4788  ssnlim  4804  ssimaex  5728  weniso  6015  sorpsscmpl  6470  canth  6476  oeeulem  6781  nnawordex  6817  elpmg  6969  fineqvlem  7260  supub  7398  suplub  7399  ordtypelem6  7426  ordtypelem7  7427  hartogslem1  7445  hartogs  7447  wemapso2lem  7453  card2on  7456  elharval  7465  wdom2d  7482  cantnfs  7555  oemapvali  7574  rankuni2b  7713  scottex  7743  tskwe  7771  cardid2  7774  iscard2  7797  harval2  7818  cardmin2  7819  acni3  7862  alephsuc2  7895  kmlem1  7964  cofsmo  8083  coftr  8087  fin23lem11  8131  enfin2i  8135  fin1a2lem9  8222  fin1a2lem11  8224  axcc4  8253  axdc3lem2  8265  zorn2lem7  8316  ondomon  8372  alephval2  8381  grutsk  8631  pinq  8738  infm3  9900  infmrcl  9920  nnind  9951  peano2uz2  10290  peano5uzi  10291  dfuzi  10293  uzind  10294  uzind3  10296  uzind3OLD  10298  eluz1  10425  uzind4  10467  nnwos  10477  eqreznegel  10494  zsupss  10498  zmin  10503  elixx1  10858  elioo2  10890  elfz1  10981  flval3  11150  serge0  11305  expge0  11344  expge1  11345  hashbclem  11629  shftf  11822  rlimrege0  12301  incexc2  12546  divalglem4  12844  divalgmod  12854  bitsval  12864  bezout  12970  1nprm  13012  1idssfct  13013  isprm2  13015  phicl2  13085  hashdvds  13092  odzval  13105  odzcllem  13106  odzdvds  13109  pcpremul  13145  prmreclem1  13212  prmreclem2  13213  prmreclem3  13214  prmreclem5  13216  ramub  13309  rami  13311  ramub1lem1  13322  ramub1lem2  13323  ismre  13743  mrcflem  13759  mrcval  13763  ismri  13784  isacs  13804  isacs1i  13810  catlid  13836  catrid  13837  ismon  13887  isnat  14072  eldmcoa  14148  coaval  14151  ismhm  14668  issubm  14676  mhmeql  14692  gsumress  14705  gsumval2  14711  grplinv  14779  issubg  14872  cycsubg  14896  isnsg  14897  ghmeql  14956  isgim  14977  isga  14996  elcntz  15049  elcntzsn  15052  odid  15104  odlem2  15105  gexid  15143  gexlem2  15144  gexdvds  15146  isslw  15170  pgpssslw  15176  pj1id  15259  efgsfo  15299  oddvdssubg  15398  pgpfac1lem5  15565  ablfaclem2  15572  isirred  15732  issubrg  15796  isabv  15835  islss  15939  islmhm  16031  lmhmeql  16059  islmim  16062  islbs  16076  gsumbagdiaglem  16368  psrmulcllem  16379  psrlidm  16395  psrridm  16396  psrass1  16397  psrcom  16400  mplsubglem  16426  mpllsslem  16427  mplmonmul  16455  coe1mul2  16590  elocv  16819  isobs  16871  istopon  16914  fctop  16992  cctop  16994  ppttop  16995  pptbas  16996  epttop  16997  iscld  17015  clscld  17035  isnei  17091  neips  17101  neiptopnei  17120  iscn  17222  iscnp  17224  ordthauslem  17370  cmpsublem  17385  concompcon  17417  2ndc1stc  17436  2ndcdisj  17441  elkgen  17490  xkoopn  17543  xkoccn  17573  txdis1cn  17589  pthaus  17592  txkgen  17606  xkohaus  17607  xkococnlem  17613  xkococn  17614  xkoinjcn  17641  txcon  17643  elqtop  17651  nrmr0reg  17703  elmptrab  17781  fbssfi  17791  opnfbas  17796  elfg  17825  cfinfil  17847  csdfil  17848  supfil  17849  filssufilg  17865  uffix  17875  fixufil  17876  uffixfr  17877  uffixsn  17879  ufinffr  17883  ufilen  17884  elflim2  17918  supnfcls  17974  fclscf  17979  flimfnfcls  17982  alexsubALTlem2  18001  alexsubALTlem4  18003  alexsubALT  18004  ptcmplem2  18006  tmdgsum2  18048  symgtgp  18053  ghmcnp  18066  elutop  18185  isucn  18230  iscfilu  18240  ismet  18263  isxmet  18264  elbl  18324  restmetu  18490  icccmp  18728  elcncf  18791  ishtpy  18869  isphtpy  18878  om1elbas  18929  iscfil  19090  iscau  19101  iscmet  19109  lmle  19126  minveclem3  19198  minveclem4  19201  ovolshftlem1  19273  ovolscalem1  19277  ovolicc2lem3  19283  iundisj  19310  dyadmax  19358  dyadmbllem  19359  opnmbllem  19361  vitalilem2  19369  vitalilem3  19370  elcpn  19688  evlsval2  19809  ig1pval3  19965  coelem  20013  quotlem  20085  elqaalem1  20104  elqaalem3  20106  aannenlem1  20113  aannenlem2  20114  aalioulem2  20118  radcnv0  20200  dmarea  20664  jensen  20695  ftalem4  20726  ftalem5  20727  efnnfsumcl  20753  efchtdvds  20810  sqff1o  20833  dvdsdivcl  20834  fsumdvdsdiaglem  20836  dvdsppwf1o  20839  dvdsflf1o  20840  dvdsflsumcom  20841  musum  20844  muinv  20846  logfac2  20869  dchrelbas  20888  dchrfi  20907  lgsfle1  20957  lgsle1  20963  lgsdirprm  20981  lgsne0  20985  lgsquadlem1  21006  lgsquadlem2  21007  dchrvmasumlem1  21057  logsqvma  21104  pntleml  21173  umgrale  21224  umgra1  21229  uslgra1  21260  usgra1  21261  usgraedg2  21263  usgraedgrnv  21265  usgrarnedg  21271  usgraedg4  21273  usgraexmpl  21287  usgrares1  21291  nbgrael  21305  nbgraeledg  21309  nbgraf1olem3  21320  cusgrarn  21335  nbcusgra  21339  cusgrares  21348  uvtxel  21365  uvtxnbgra  21369  cusgrauvtxb  21372  eupath2  21551  umgrabi  21554  konigsberg  21558  grpoidinv2  21655  grpoinv  21664  isssp  22072  islno  22103  isblo  22132  ishmo  22161  ubthlem1  22221  ubthlem2  22222  htthlem  22269  ocel  22632  shsval2i  22738  ococin  22759  chsupsn  22764  eleigvec  23309  cnlnadjlem5  23423  shatomistici  23713  hatomistici  23714  indf1ofs  24220  sigagenval  24320  ismbfm  24397  imambfm  24407  dya2iocuni  24428  dstfrvel  24511  ballotlemfc0  24530  ballotlemfcc  24531  ballotlemiex  24539  ballotlemfrcn0  24567  ballotlemirc  24569  ballotlem7  24573  conpcon  24702  iscvm  24726  cvmsi  24732  cvmsval  24733  cvmliftmolem2  24749  cvmliftiota  24768  snmlval  24798  elgiso  24887  sltval2  25335  sltres  25343  nodenselem7  25366  nofulllem5  25385  lineelsb2  25797  linerflx1  25798  rankeq1o  25827  itg2gt0cn  25961  finminlem  26013  fneint  26049  fnessref  26065  locfincmp  26076  topmeet  26085  topjoin  26086  neifg  26092  indexa  26127  nninfnub  26147  istotbnd  26170  sstotbnd2  26175  isbnd  26181  isrngohom  26273  isrngoiso  26286  isidl  26316  ispridl  26336  ismaxidl  26342  prnc  26369  isfldidl  26370  isnacs  26450  elmzpcl  26475  mzpindd  26495  rencldnfilem  26573  irrapxlem6  26582  pellexlem3  26586  pellexlem5  26588  elpell1qr  26602  elpell14qr  26604  elpell1234qr  26606  pellfundre  26636  pellfundge  26637  pellfundlb  26639  pellfundglb  26640  rmspecnonsq  26662  jm2.22  26758  jm2.23  26759  rpnnen3lem  26794  fnwe2lem2  26818  fnwe2lem3  26819  dsmmelbas  26875  frlmelbas  26894  frlmssuvc2  26917  islinds  26949  elmnc  27011  dgraalem  27020  dgraaub  27023  mpaalem  27027  rgspnmin  27046  issubmd  27053  pmtrval  27064  pmtrrn  27069  symgsssg  27078  symgfisg  27079  psgnunilem5  27087  issdrg  27175  phisum  27188  stoweidlem14  27432  stoweidlem15  27433  stoweidlem16  27434  stoweidlem31  27449  stoweidlem36  27454  stoweidlem46  27464  stoweidlem48  27466  secval  27837  cscval  27838  cotval  27839  islshp  29095  lssats  29128  islfl  29176  isat  29402  atlatmstc  29435  islln  29621  islpln  29645  islvol  29688  linepsubN  29867  elpmap  29873  pmapsub  29883  elpadd  29914  paddvaln0N  29916  islhp  30111  isldil  30225  isltrn  30234  isdilN  30269  istrnN  30272  diaval  31148  diaelval  31149  diaeldm  31152  diaelrnN  31161  cdlemm10N  31234  docaclN  31240  dibglbN  31282  dicval  31292  dicfnN  31299  dicvalrelN  31301  dihglblem2aN  31409  dihglblem2N  31410  dihglblem3N  31411  dih1dimatlem  31445  dihglb2  31458  dochvalr  31473  doch2val2  31480  dochocss  31482  islpolN  31599  mapd0  31781
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-rab 2659  df-v 2902
  Copyright terms: Public domain W3C validator