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

Theorem elrab 3230
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 2585 . 2  |-  F/_ x A
2 nfcv 2585 . 2  |-  F/_ x B
3 nfv 1752 . 2  |-  F/ x ps
4 elrab.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
51, 2, 3, 4elrabf 3228 1  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1438    e. wcel 1869   {crab 2780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-rab 2785  df-v 3084
This theorem is referenced by:  elrab3  3231  elrab2  3232  ralrab  3234  rexrab  3236  rabsnt  4075  unimax  4252  ssintub  4271  intminss  4280  rabxfrd  4640  ssimaex  5944  weniso  6258  canth  6262  sorpsscmpl  6594  onnminsb  6643  dfom2  6706  ssnlim  6722  elsuppfn  6931  ressuppssdif  6945  oeeulem  7308  nnawordex  7344  elpmg  7493  fineqvlem  7790  mapfienlem2  7923  supub  7977  suplub  7978  ordtypelem6  8042  ordtypelem7  8043  hartogslem1  8061  hartogs  8063  wemapsolem  8069  card2on  8073  elharval  8082  wdom2d  8099  cantnfs  8174  oemapvali  8192  rankuni2b  8327  scottex  8359  tskwe  8387  cardid2  8390  iscard2  8413  harval2  8434  cardmin2  8435  acni3  8480  alephsuc2  8513  kmlem1  8582  cofsmo  8701  coftr  8705  fin23lem11  8749  enfin2i  8753  fin1a2lem9  8840  fin1a2lem11  8842  axcc4  8871  axdc3lem2  8883  zorn2lem7  8934  ondomon  8990  alephval2  8999  grutsk  9249  pinq  9354  negf1o  10051  fiminre  10557  infm3  10570  infmrclOLD  10595  nnind  10629  peano2uz2  11025  peano5uzi  11026  dfuzi  11028  uzind  11029  uzind3  11031  eluz1  11165  uzind4  11219  nnwos  11228  eqreznegel  11251  zsupss  11255  zmin  11262  elixx1  11646  elioo2  11679  elfz1  11791  flval3  12051  serge0  12268  expge0  12309  expge1  12310  hashbclem  12614  pr2pwpr  12634  elss2pr  12643  wrdmap  12696  wwlktovfo  13027  shftf  13136  rlimrege0  13636  incexc2  13889  divalglem4  14368  divalgmod  14380  bitsval  14390  bezout  14503  lcmledvds  14557  lcmgcdlem  14564  lcmsledvdsOLD  14578  lcmfledvds  14598  1nprm  14622  1idssfct  14623  isprm2  14625  phicl2  14709  hashdvds  14716  odzval  14729  odzcllem  14730  odzdvds  14733  odzvalOLD  14735  odzcllemOLD  14736  odzdvdsOLD  14739  pcpremul  14786  prmreclem1  14853  prmreclem2  14854  prmreclem3  14855  prmreclem5  14857  ramub  14963  rami  14965  ramub1lem1  14977  ramub1lem2  14978  prmgaplem3  15016  prmgaplem4  15017  prmgaplem5  15018  prmgaplem6  15019  ismre  15489  mrcflem  15505  mrcval  15509  ismri  15530  isacs  15550  isacs1i  15556  catlid  15582  catrid  15583  ismon  15631  isnat  15845  eldmcoa  15953  coaval  15956  fncnvimaeqv  15998  lubeldm  16220  glbeldm  16233  gsumress  16512  gsumval2  16516  ismhm  16577  issubm  16587  issubmd  16589  mhmeql  16604  mrcmndind  16606  grplinv  16705  issubg  16810  cycsubg  16838  isnsg  16839  ghmeql  16898  isgim  16919  isga  16938  elcntz  16969  elcntzsn  16972  symgfix2  17050  pmtrval  17085  pmtrrn  17091  symgsssg  17101  symgfisg  17102  psgnunilem5  17128  odid  17180  odlem2  17181  odidOLD  17196  odlem2OLD  17197  gexid  17225  gexlem2  17226  gexdvds  17228  gexlem2OLD  17229  isslw  17253  pgpssslw  17259  pj1id  17342  efgsfo  17382  oddvdssubg  17486  dprdwd  17636  pgpfac1lem5  17705  ablfaclem2  17712  isirred  17920  isrim0  17944  issubrg  18001  isabv  18040  islss  18151  islmhm  18243  lmhmeql  18271  islmim  18278  islbs  18292  gsumbagdiaglem  18592  psrmulcllem  18604  psrlidm  18620  psrridm  18621  psrass1  18622  psrcom  18626  mplsubglem  18651  mpllsslem  18652  mplmonmul  18681  evlsval2  18736  coe1fsupp  18800  coe1ae0  18802  coe1mul2  18855  zrhcofipsgn  19153  psgndiflemB  19160  elocv  19223  isobs  19275  dsmmelbas  19294  frlmelbas  19311  frlmssuvc2  19345  islinds  19359  dmatel  19510  dmatmulcl  19517  scmatel  19522  scmateALT  19529  symgmatr01lem  19670  pmatcoe1fsupp  19717  cpmatel  19727  chpscmat  19858  istopon  19932  fctop  20011  cctop  20013  ppttop  20014  pptbas  20015  epttop  20016  iscld  20034  clscld  20054  isnei  20111  neips  20121  neiptopnei  20140  iscn  20243  iscnp  20245  ordthauslem  20391  cmpsublem  20406  concompcon  20439  2ndc1stc  20458  2ndcdisj  20463  locfincmp  20533  elkgen  20543  xkoopn  20596  xkoccn  20626  txdis1cn  20642  pthaus  20645  txkgen  20659  xkohaus  20660  xkococnlem  20666  xkococn  20667  xkoinjcn  20694  txcon  20696  elqtop  20704  nrmr0reg  20756  elmptrab  20834  fbssfi  20844  opnfbas  20849  elfg  20878  cfinfil  20900  csdfil  20901  supfil  20902  filssufilg  20918  uffix  20928  fixufil  20929  uffixfr  20930  uffixsn  20932  ufinffr  20936  ufilen  20937  elflim2  20971  supnfcls  21027  fclscf  21032  flimfnfcls  21035  alexsubALTlem2  21055  alexsubALTlem4  21057  alexsubALT  21058  ptcmplem2  21060  tmdgsum2  21103  symgtgp  21108  ghmcnp  21121  elutop  21240  isucn  21285  iscfilu  21295  ispsmet  21312  ismet  21330  isxmet  21331  elblps  21394  elbl  21395  restmetu  21577  icccmp  21835  elcncf  21913  ishtpy  21995  isphtpy  22004  om1elbas  22055  iscfil  22227  iscau  22238  iscmet  22246  lmle  22263  rrxfsupp  22348  minveclem3  22363  minveclem4  22366  minveclem3OLD  22375  minveclem4OLD  22378  ovolshftlem1  22454  ovolscalem1  22458  ovolicc2lem3  22464  iundisj  22493  dyadmax  22548  dyadmbllem  22549  opnmbllem  22551  vitalilem2  22559  vitalilem3  22560  elcpn  22880  ig1pval3  23118  ig1pval3OLD  23124  coelem  23172  quotlem  23245  elqaalem1  23264  elqaalem3  23266  elqaalem1OLD  23267  elqaalem3OLD  23269  aannenlem1  23276  aannenlem2  23277  aalioulem2  23281  radcnv0  23363  dmarea  23875  jensen  23906  ftalem4  23992  ftalem5  23993  ftalem4OLD  23994  ftalem5OLD  23995  efnnfsumcl  24021  efchtdvds  24078  sqff1o  24101  dvdsdivcl  24102  fsumdvdsdiaglem  24104  dvdsppwf1o  24107  dvdsflf1o  24108  dvdsflsumcom  24109  musum  24112  muinv  24114  logfac2  24137  dchrelbas  24156  dchrfi  24175  lgsfle1  24225  lgsle1  24231  lgsdirprm  24249  lgsne0  24253  lgsquadlem1  24274  lgsquadlem2  24275  dchrvmasumlem1  24325  logsqvma  24372  pntleml  24441  tgellng  24590  mircgr  24694  mirbtwn  24695  iseqlg  24889  ttgelitv  24905  umgrale  25040  umgra1  25045  edg  25072  uslgra1  25091  usgra1  25092  usgraedg2  25094  usgraedgrnv  25096  usgrarnedg  25103  usgraedg4  25106  usgraexmplef  25120  usgrares1  25130  nbgrael  25146  nbgraeledg  25150  nbgraf1olem3  25163  cusgrarn  25179  nbcusgra  25183  cusgrares  25192  uvtxel  25209  uvtxnbgra  25213  cusgrauvtxb  25216  iswwlk  25403  iswwlkn  25404  wlknwwlknsur  25432  wlkiswwlksur  25439  wwlkextsur  25451  wlknwwlknvbij  25460  isclwwlk  25488  isclwwlkn  25489  clwwlkprop  25490  clwwlknprop  25492  clwwlkvbij  25521  clwwlknscsh  25539  eleclclwwlkn  25553  el2wlkonot  25589  el2spthonot  25590  el2spthonot0  25591  el2wlksoton  25598  el2spthsoton  25599  el2wlksotot  25602  rusgranumwlklem0  25668  rusgranumwlklem1  25669  rusgranumwlklem3  25671  rusgranumwlks  25676  eupath2  25700  umgrabi  25703  konigsberg  25707  2spotdisj  25781  usg2spot2nb  25785  usgreg2spot  25787  numclwwlkun  25799  numclwwlkovfel2  25803  numclwwlkovgel  25808  numclwlk1lem2foa  25811  numclwwlk2lem1  25822  numclwlk2lem2f  25823  numclwlk2lem2f1o  25825  grpoidinv2  25938  grpoinv  25947  isssp  26355  islno  26386  isblo  26415  ishmo  26444  ubthlem1  26504  ubthlem2  26505  htthlem  26562  ocel  26926  shsval2i  27032  ococin  27053  chsupsn  27058  eleigvec  27602  cnlnadjlem5  27716  shatomistici  28006  hatomistici  28007  nnindf  28383  ordtconlem1  28732  indf1ofs  28849  sigagenval  28964  ldsysgenld  28984  ldgenpisyslem1  28987  ldgenpisyslem2  28988  ldgenpisys  28990  ddemeas  29061  ismbfm  29076  imambfm  29086  dya2iocuni  29107  oms0  29127  omssubadd  29130  oms0OLD  29131  omssubaddOLD  29134  elcarsg  29139  issibf  29168  sitgfval  29176  oddpwdc  29189  eulerpartlemgh  29213  eulerpartlemgs2  29215  dstfrvel  29308  ballotlemfc0  29327  ballotlemfcc  29328  ballotlemiex  29336  ballotlemfrcn0  29364  ballotlemirc  29366  ballotlem7  29370  ballotlemiexOLD  29374  ballotlemfrcn0OLD  29402  ballotlemircOLD  29404  ballotlem7OLD  29408  conpcon  29960  iscvm  29984  cvmsi  29990  cvmsval  29991  cvmliftmolem2  30007  cvmliftiota  30026  snmlval  30056  elmpst  30176  elgiso  30316  sltval2  30544  sltres  30552  nodenselem7  30575  nofulllem5  30594  lineelsb2  30914  linerflx1  30915  fwddifval  30928  fwddifnval  30929  rankeq1o  30937  finminlem  30973  fneint  31003  fnessref  31012  topmeet  31019  topjoin  31020  neifg  31026  relowlssretop  31724  fin2solem  31889  fin2so  31890  poimirlem4  31902  poimirlem25  31923  poimirlem26  31924  poimirlem27  31925  poimirlem31  31929  poimirlem32  31930  opnmbllem0  31934  mblfinlem2  31936  itg2gt0cn  31955  indexa  32018  nninfnub  32038  istotbnd  32059  sstotbnd2  32064  isbnd  32070  isrngohom  32162  isrngoiso  32175  isidl  32205  ispridl  32225  ismaxidl  32231  prnc  32258  isfldidl  32259  islshp  32508  lssats  32541  islfl  32589  isat  32815  atlatmstc  32848  islln  33034  islpln  33058  islvol  33101  linepsubN  33280  elpmap  33286  pmapsub  33296  elpadd  33327  paddvaln0N  33329  islhp  33524  isldil  33638  isltrn  33647  isdilN  33683  istrnN  33686  diaval  34563  diaelval  34564  diaeldm  34567  diaelrnN  34576  cdlemm10N  34649  docaclN  34655  dibglbN  34697  dicval  34707  dicfnN  34714  dicvalrelN  34716  dihglblem2aN  34824  dihglblem2N  34825  dihglblem3N  34826  dih1dimatlem  34860  dihglb2  34873  dochvalr  34888  doch2val2  34895  dochocss  34897  islpolN  35014  mapd0  35196  isnacs  35509  elmzpcl  35531  mzpindd  35551  rencldnfilem  35626  irrapxlem6  35635  pellexlem3  35639  pellexlem5  35641  elpell1qr  35657  elpell14qr  35659  elpell1234qr  35661  pellfundre  35693  pellfundge  35694  pellfundlb  35696  pellfundglb  35697  rmspecnonsq  35719  jm2.22  35814  jm2.23  35815  rpnnen3lem  35850  fnwe2lem2  35873  fnwe2lem3  35874  elmnc  35959  dgraalem  35971  dgraalemOLD  35972  dgraaub  35977  dgraaubOLD  35978  mpaalem  35982  rgspnmin  36001  issdrg  36027  phisum  36040  nzss  36568  iccshift  37494  iooshift  37498  limcperiod  37572  sumnnodd  37574  ioodvbdlimc1lem1  37667  ioodvbdlimc1lem1OLD  37669  dvnprodlem1  37685  dvnprodlem3  37687  itgperiod  37722  stoweidlem14  37738  stoweidlem15  37739  stoweidlem16  37740  stoweidlem31  37756  stoweidlem36  37761  stoweidlem46  37771  stoweidlem48  37773  fourierdlem2  37835  fourierdlem3  37836  fourierdlem20  37853  fourierdlem25  37858  fourierdlem37  37871  fourierdlem42  37876  fourierdlem42OLD  37877  fourierdlem48  37882  fourierdlem51  37885  fourierdlem63  37897  fourierdlem64  37898  fourierdlem65  37899  fourierdlem79  37913  fourierdlem81  37915  elaa2lem  37961  elaa2lemOLD  37962  etransclem24  37987  etransclem26  37989  etransclem28  37991  etransclem35  37998  etransclem48OLD  38011  etransclem48  38012  salgenval  38027  salgencl  38035  sge0fodjrnlem  38090  meadjiunlem  38126  caragenel  38139  ovnlecvr  38199  ovnpnfelsup  38200  ovncvrrp  38205  ovnsubaddlem1  38211  iccpart  38486  iseven  38513  isodd  38514  dfodd2  38522  dfeven5  38552  dfodd7  38553  umgrle  38887  umgr1lem  38893  edga  38921  usgruspgrb  38937  usgredg2  38944  usgredgedga  38969  ismgmhm  39125  issubmgm  39131  rabsubmgmd  39133  mgmhmeql  39145  assintop  39187  isassintop  39188  assintopcllaw  39190  isrnghm  39234  isrngisom  39238  0even  39273  2even  39275  2zrngamgm  39281  dmatALTbasel  39539  lcoval  39549  elbigo  39706  secval  39811  cscval  39812  cotval  39813
  Copyright terms: Public domain W3C validator