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

Theorem elrab 3224
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 2616 . 2  |-  F/_ x A
2 nfcv 2616 . 2  |-  F/_ x B
3 nfv 1674 . 2  |-  F/ x ps
4 elrab.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
51, 2, 3, 4elrabf 3222 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 1370    e. wcel 1758   {crab 2803
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2808  df-v 3080
This theorem is referenced by:  elrab3  3225  elrab2  3226  ralrab  3228  rexrab  3230  rabsnt  4061  unimax  4236  ssintub  4255  intminss  4263  reusv6OLD  4612  rabxfrd  4622  ssimaex  5866  weniso  6155  canth  6159  sorpsscmpl  6482  onnminsb  6526  dfom2  6589  ssnlim  6605  elsuppfn  6809  ressuppssdif  6821  oeeulem  7151  nnawordex  7187  elpmg  7339  fineqvlem  7639  mapfienlem2  7767  supub  7821  suplub  7822  ordtypelem6  7849  ordtypelem7  7850  hartogslem1  7868  hartogs  7870  wemapsolem  7876  card2on  7881  elharval  7890  wdom2d  7907  cantnfs  7986  oemapvali  8004  cantnfsOLD  8016  rankuni2b  8172  scottex  8204  tskwe  8232  cardid2  8235  iscard2  8258  harval2  8279  cardmin2  8280  acni3  8329  alephsuc2  8362  kmlem1  8431  cofsmo  8550  coftr  8554  fin23lem11  8598  enfin2i  8602  fin1a2lem9  8689  fin1a2lem11  8691  axcc4  8720  axdc3lem2  8732  zorn2lem7  8783  ondomon  8839  alephval2  8848  grutsk  9101  pinq  9208  infm3  10401  infmrcl  10421  nnind  10452  peano2uz2  10841  peano5uzi  10842  dfuzi  10844  uzind  10845  uzind3  10847  uzind3OLD  10849  eluz1  10977  uzind4  11024  nnwos  11034  eqreznegel  11052  zsupss  11056  zmin  11061  elixx1  11421  elioo2  11453  elfz1  11560  flval3  11781  serge0  11978  expge0  12018  expge1  12019  pr2pwpr  12302  hashbclem  12324  disjxwrd  12468  shftf  12687  rlimrege0  13176  incexc2  13420  divalglem4  13719  divalgmod  13729  bitsval  13739  bezout  13845  1nprm  13887  1idssfct  13888  isprm2  13890  phicl2  13962  hashdvds  13969  odzval  13982  odzcllem  13983  odzdvds  13986  pcpremul  14029  prmreclem1  14096  prmreclem2  14097  prmreclem3  14098  prmreclem5  14100  ramub  14193  rami  14195  ramub1lem1  14206  ramub1lem2  14207  ismre  14648  mrcflem  14664  mrcval  14668  ismri  14689  isacs  14709  isacs1i  14715  catlid  14741  catrid  14742  ismon  14792  isnat  14977  eldmcoa  15053  coaval  15056  lubeldm  15271  glbeldm  15284  ismhm  15586  issubm  15595  issubmd  15597  mhmeql  15612  mrcmndind  15614  gsumress  15627  gsumval2  15633  grplinv  15704  issubg  15801  cycsubg  15829  isnsg  15830  ghmeql  15889  isgim  15910  isga  15929  elcntz  15960  elcntzsn  15963  symgfix2  16041  pmtrval  16077  pmtrrn  16083  symgsssg  16093  symgfisg  16094  psgnunilem5  16120  odid  16163  odlem2  16164  gexid  16202  gexlem2  16203  gexdvds  16205  isslw  16229  pgpssslw  16235  pj1id  16318  efgsfo  16358  oddvdssubg  16459  pgpfac1lem5  16703  ablfaclem2  16710  isirred  16915  isrim0  16937  issubrg  16989  isabv  17028  islss  17140  islmhm  17232  lmhmeql  17260  islmim  17267  islbs  17281  gsumbagdiaglem  17569  psrmulcllem  17582  psrlidm  17598  psrlidmOLD  17599  psrridm  17600  psrridmOLD  17601  psrass1  17602  psrcom  17606  mplsubglem  17635  mpllsslem  17636  mplsubglemOLD  17637  mpllsslemOLD  17638  mplmonmul  17668  evlsval2  17731  coe1mul2  17847  zrhcofipsgn  18149  psgndiflemB  18156  elocv  18219  isobs  18271  dsmmelbas  18290  frlmelbas  18308  frlmelbasOLD  18309  frlmssuvc2  18346  frlmssuvc2OLD  18348  islinds  18364  symgmatr01lem  18592  istopon  18663  fctop  18741  cctop  18743  ppttop  18744  pptbas  18745  epttop  18746  iscld  18764  clscld  18784  isnei  18840  neips  18850  neiptopnei  18869  iscn  18972  iscnp  18974  ordthauslem  19120  cmpsublem  19135  concompcon  19169  2ndc1stc  19188  2ndcdisj  19193  elkgen  19242  xkoopn  19295  xkoccn  19325  txdis1cn  19341  pthaus  19344  txkgen  19358  xkohaus  19359  xkococnlem  19365  xkococn  19366  xkoinjcn  19393  txcon  19395  elqtop  19403  nrmr0reg  19455  elmptrab  19533  fbssfi  19543  opnfbas  19548  elfg  19577  cfinfil  19599  csdfil  19600  supfil  19601  filssufilg  19617  uffix  19627  fixufil  19628  uffixfr  19629  uffixsn  19631  ufinffr  19635  ufilen  19636  elflim2  19670  supnfcls  19726  fclscf  19731  flimfnfcls  19734  alexsubALTlem2  19753  alexsubALTlem4  19755  alexsubALT  19756  ptcmplem2  19758  tmdgsum2  19800  symgtgp  19805  ghmcnp  19818  elutop  19941  isucn  19986  iscfilu  19996  ispsmet  20013  ismet  20031  isxmet  20032  elblps  20095  elbl  20096  restmetu  20295  icccmp  20535  elcncf  20598  ishtpy  20677  isphtpy  20686  om1elbas  20737  iscfil  20909  iscau  20920  iscmet  20928  lmle  20945  rrxfsupp  21034  minveclem3  21049  minveclem4  21052  ovolshftlem1  21125  ovolscalem1  21129  ovolicc2lem3  21135  iundisj  21163  dyadmax  21212  dyadmbllem  21213  opnmbllem  21215  vitalilem2  21223  vitalilem3  21224  elcpn  21542  ig1pval3  21780  coelem  21828  quotlem  21900  elqaalem1  21919  elqaalem3  21921  aannenlem1  21928  aannenlem2  21929  aalioulem2  21933  radcnv0  22015  dmarea  22485  jensen  22516  ftalem4  22547  ftalem5  22548  efnnfsumcl  22574  efchtdvds  22631  sqff1o  22654  dvdsdivcl  22655  fsumdvdsdiaglem  22657  dvdsppwf1o  22660  dvdsflf1o  22661  dvdsflsumcom  22662  musum  22665  muinv  22667  logfac2  22690  dchrelbas  22709  dchrfi  22728  lgsfle1  22778  lgsle1  22784  lgsdirprm  22802  lgsne0  22806  lgsquadlem1  22827  lgsquadlem2  22828  dchrvmasumlem1  22878  logsqvma  22925  pntleml  22994  tgellng  23124  mircgr  23205  mirbtwn  23206  ttgelitv  23282  ebtwntg  23381  umgrale  23408  umgra1  23413  uslgra1  23444  usgra1  23445  usgraedg2  23447  usgraedgrnv  23449  usgrarnedg  23456  usgraedg4  23458  usgraexmpl  23472  usgrares1  23476  nbgrael  23490  nbgraeledg  23494  nbgraf1olem3  23505  cusgrarn  23520  nbcusgra  23524  cusgrares  23533  uvtxel  23550  uvtxnbgra  23554  cusgrauvtxb  23557  eupath2  23754  umgrabi  23757  konigsberg  23761  grpoidinv2  23858  grpoinv  23867  isssp  24275  islno  24306  isblo  24335  ishmo  24364  ubthlem1  24424  ubthlem2  24425  htthlem  24472  ocel  24837  shsval2i  24943  ococin  24964  chsupsn  24969  eleigvec  25514  cnlnadjlem5  25628  shatomistici  25918  hatomistici  25919  nnindf  26235  ordtconlem1  26500  indf1ofs  26628  sigagenval  26729  ddemeas  26797  ismbfm  26812  imambfm  26822  dya2iocuni  26843  oms0  26855  issibf  26864  sitgfval  26872  oddpwdc  26882  eulerpartlemgh  26906  eulerpartlemgs2  26908  dstfrvel  27001  ballotlemfc0  27020  ballotlemfcc  27021  ballotlemiex  27029  ballotlemfrcn0  27057  ballotlemirc  27059  ballotlem7  27063  conpcon  27269  iscvm  27293  cvmsi  27299  cvmsval  27300  cvmliftmolem2  27316  cvmliftiota  27335  snmlval  27365  elgiso  27460  sltval2  27942  sltres  27950  nodenselem7  27973  nofulllem5  27992  lineelsb2  28324  linerflx1  28325  rankeq1o  28354  fin2solem  28564  fin2so  28565  opnmbllem0  28576  mblfinlem2  28578  itg2gt0cn  28596  finminlem  28662  fneint  28698  fnessref  28714  locfincmp  28725  topmeet  28734  topjoin  28735  neifg  28741  indexa  28776  nninfnub  28796  istotbnd  28817  sstotbnd2  28822  isbnd  28828  isrngohom  28920  isrngoiso  28933  isidl  28963  ispridl  28983  ismaxidl  28989  prnc  29016  isfldidl  29017  isnacs  29189  elmzpcl  29211  mzpindd  29231  rencldnfilem  29308  irrapxlem6  29317  pellexlem3  29321  pellexlem5  29323  elpell1qr  29337  elpell14qr  29339  elpell1234qr  29341  pellfundre  29371  pellfundge  29372  pellfundlb  29374  pellfundglb  29375  rmspecnonsq  29397  jm2.22  29493  jm2.23  29494  rpnnen3lem  29529  fnwe2lem2  29553  fnwe2lem3  29554  elmnc  29642  dgraalem  29651  dgraaub  29654  mpaalem  29658  rgspnmin  29677  issdrg  29703  phisum  29716  stoweidlem14  29958  stoweidlem15  29959  stoweidlem16  29960  stoweidlem31  29975  stoweidlem36  29980  stoweidlem46  29990  stoweidlem48  29992  elss2pr  30377  wwlktovf  30400  wwlktovf1  30401  wwlktovfo  30402  iswwlk  30466  iswwlkn  30467  wlknwwlknsur  30493  wlkiswwlksur  30500  wwlkextinj  30511  wwlkextsur  30512  wlknwwlknvbij  30521  el2wlkonot  30537  el2spthonot  30538  el2spthonot0  30539  el2wlksoton  30546  el2spthsoton  30547  el2wlksotot  30550  isclwwlk  30580  isclwwlkn  30581  clwwlkprop  30582  clwwlknprop  30584  clwwlkvbij  30612  Lemma2  30642  eleclclwwlkn  30656  clwlkfclwwlk1hashn  30663  clwlkf1clwwlklem1  30668  clwlkf1clwwlklem2  30669  rusgranumwlklem0  30715  rusgranumwlklem1  30716  rusgranumwlklem3  30718  rusgranumwlks  30723  2spotdisj  30803  usg2spot2nb  30807  usgreg2spot  30809  numclwwlkun  30821  numclwwlkovfel2  30825  numclwwlkovgel  30830  numclwlk1lem2foa  30833  numclwwlk2lem1  30844  numclwlk2lem2f  30845  numclwlk2lem2f1o  30847  coe1fsupp  30985  coe1ae0  30986  scmatscmids  31027  dmatbasel  31051  dmatelnd  31055  dmatsubcl  31057  dmatmulcl  31059  scmatsubcl  31064  scmatmulcl  31066  lcoval  31079  pmatcoe1fsupp  31193  cpmatel  31201  cpscmat  31329  secval  31411  cscval  31412  cotval  31413  islshp  32963  lssats  32996  islfl  33044  isat  33270  atlatmstc  33303  islln  33489  islpln  33513  islvol  33556  linepsubN  33735  elpmap  33741  pmapsub  33751  elpadd  33782  paddvaln0N  33784  islhp  33979  isldil  34093  isltrn  34102  isdilN  34137  istrnN  34140  diaval  35016  diaelval  35017  diaeldm  35020  diaelrnN  35029  cdlemm10N  35102  docaclN  35108  dibglbN  35150  dicval  35160  dicfnN  35167  dicvalrelN  35169  dihglblem2aN  35277  dihglblem2N  35278  dihglblem3N  35279  dih1dimatlem  35313  dihglb2  35326  dochvalr  35341  doch2val2  35348  dochocss  35350  islpolN  35467  mapd0  35649
  Copyright terms: Public domain W3C validator