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

Theorem elrab 3195
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 2591 . 2  |-  F/_ x A
2 nfcv 2591 . 2  |-  F/_ x B
3 nfv 1760 . 2  |-  F/ x ps
4 elrab.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
51, 2, 3, 4elrabf 3193 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 1443    e. wcel 1886   {crab 2740
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-rab 2745  df-v 3046
This theorem is referenced by:  elrab3  3196  elrab2  3197  ralrab  3199  rexrab  3201  rabsnt  4048  unimax  4232  ssintub  4251  intminss  4260  rabxfrd  4620  ssimaex  5928  weniso  6243  canth  6247  sorpsscmpl  6579  onnminsb  6628  dfom2  6691  ssnlim  6707  elsuppfn  6919  ressuppssdif  6933  oeeulem  7299  nnawordex  7335  elpmg  7484  fineqvlem  7783  mapfienlem2  7916  supub  7970  suplub  7971  ordtypelem6  8035  ordtypelem7  8036  hartogslem1  8054  hartogs  8056  wemapsolem  8062  card2on  8066  elharval  8075  wdom2d  8092  cantnfs  8168  oemapvali  8186  rankuni2b  8321  scottex  8353  tskwe  8381  cardid2  8384  iscard2  8407  harval2  8428  cardmin2  8429  acni3  8475  alephsuc2  8508  kmlem1  8577  cofsmo  8696  coftr  8700  fin23lem11  8744  enfin2i  8748  fin1a2lem9  8835  fin1a2lem11  8837  axcc4  8866  axdc3lem2  8878  zorn2lem7  8929  ondomon  8985  alephval2  8994  grutsk  9244  pinq  9349  negf1o  10046  fiminre  10552  infm3  10565  infmrclOLD  10590  nnind  10624  peano2uz2  11020  peano5uzi  11021  dfuzi  11023  uzind  11024  uzind3  11026  eluz1  11160  uzind4  11214  nnwos  11223  eqreznegel  11246  zsupss  11250  zmin  11257  elixx1  11641  elioo2  11674  elfz1  11786  flval3  12047  serge0  12264  expge0  12305  expge1  12306  hashbclem  12612  pr2pwpr  12633  elss2prb  12640  hash2sspr  12641  elss2prOLD  12642  wrdmap  12695  wwlktovfo  13026  shftf  13135  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  19154  psgndiflemB  19161  elocv  19224  isobs  19276  dsmmelbas  19295  frlmelbas  19312  frlmssuvc2  19346  islinds  19360  dmatel  19511  dmatmulcl  19518  scmatel  19523  scmateALT  19530  symgmatr01lem  19671  pmatcoe1fsupp  19718  cpmatel  19728  chpscmat  19859  istopon  19933  fctop  20012  cctop  20014  ppttop  20015  pptbas  20016  epttop  20017  iscld  20035  clscld  20055  isnei  20112  neips  20122  neiptopnei  20141  iscn  20244  iscnp  20246  ordthauslem  20392  cmpsublem  20407  concompcon  20440  2ndc1stc  20459  2ndcdisj  20464  locfincmp  20534  elkgen  20544  xkoopn  20597  xkoccn  20627  txdis1cn  20643  pthaus  20646  txkgen  20660  xkohaus  20661  xkococnlem  20667  xkococn  20668  xkoinjcn  20695  txcon  20697  elqtop  20705  nrmr0reg  20757  elmptrab  20835  fbssfi  20845  opnfbas  20850  elfg  20879  cfinfil  20901  csdfil  20902  supfil  20903  filssufilg  20919  uffix  20929  fixufil  20930  uffixfr  20931  uffixsn  20933  ufinffr  20937  ufilen  20938  elflim2  20972  supnfcls  21028  fclscf  21033  flimfnfcls  21036  alexsubALTlem2  21056  alexsubALTlem4  21058  alexsubALT  21059  ptcmplem2  21061  tmdgsum2  21104  symgtgp  21109  ghmcnp  21122  elutop  21241  isucn  21286  iscfilu  21296  ispsmet  21313  ismet  21331  isxmet  21332  elblps  21395  elbl  21396  restmetu  21578  icccmp  21836  elcncf  21914  ishtpy  21996  isphtpy  22005  om1elbas  22056  iscfil  22228  iscau  22239  iscmet  22247  lmle  22264  rrxfsupp  22349  minveclem3  22364  minveclem4  22367  minveclem3OLD  22376  minveclem4OLD  22379  ovolshftlem1  22455  ovolscalem1  22459  ovolicc2lem3  22465  iundisj  22494  dyadmax  22549  dyadmbllem  22550  opnmbllem  22552  vitalilem2  22560  vitalilem3  22561  elcpn  22881  ig1pval3  23119  ig1pval3OLD  23125  coelem  23173  quotlem  23246  elqaalem1  23265  elqaalem3  23267  elqaalem1OLD  23268  elqaalem3OLD  23270  aannenlem1  23277  aannenlem2  23278  aalioulem2  23282  radcnv0  23364  dmarea  23876  jensen  23907  ftalem4  23993  ftalem5  23994  ftalem4OLD  23995  ftalem5OLD  23996  efnnfsumcl  24022  efchtdvds  24079  sqff1o  24102  dvdsdivcl  24103  fsumdvdsdiaglem  24105  dvdsppwf1o  24108  dvdsflf1o  24109  dvdsflsumcom  24110  musum  24113  muinv  24115  logfac2  24138  dchrelbas  24157  dchrfi  24176  lgsfle1  24226  lgsle1  24232  lgsdirprm  24250  lgsne0  24254  lgsquadlem1  24275  lgsquadlem2  24276  dchrvmasumlem1  24326  logsqvma  24373  pntleml  24442  tgellng  24591  mircgr  24695  mirbtwn  24696  iseqlg  24890  ttgelitv  24906  umgrale  25041  umgra1  25046  edg  25073  uslgra1  25092  usgra1  25093  usgraedg2  25095  usgraedgrnv  25097  usgrarnedg  25104  usgraedg4  25107  usgraexmplef  25121  usgrares1  25131  nbgrael  25147  nbgraeledg  25151  nbgraf1olem3  25164  cusgrarn  25180  nbcusgra  25184  cusgrares  25193  uvtxel  25210  uvtxnbgra  25214  cusgrauvtxb  25217  iswwlk  25404  iswwlkn  25405  wlknwwlknsur  25433  wlkiswwlksur  25440  wwlkextsur  25452  wlknwwlknvbij  25461  isclwwlk  25489  isclwwlkn  25490  clwwlkprop  25491  clwwlknprop  25493  clwwlkvbij  25522  clwwlknscsh  25540  eleclclwwlkn  25554  el2wlkonot  25590  el2spthonot  25591  el2spthonot0  25592  el2wlksoton  25599  el2spthsoton  25600  el2wlksotot  25603  rusgranumwlklem0  25669  rusgranumwlklem1  25670  rusgranumwlklem3  25672  rusgranumwlks  25677  eupath2  25701  umgrabi  25704  konigsberg  25708  2spotdisj  25782  usg2spot2nb  25786  usgreg2spot  25788  numclwwlkun  25800  numclwwlkovfel2  25804  numclwwlkovgel  25809  numclwlk1lem2foa  25812  numclwwlk2lem1  25823  numclwlk2lem2f  25824  numclwlk2lem2f1o  25826  grpoidinv2  25939  grpoinv  25948  isssp  26356  islno  26387  isblo  26416  ishmo  26445  ubthlem1  26505  ubthlem2  26506  htthlem  26563  ocel  26927  shsval2i  27033  ococin  27054  chsupsn  27059  eleigvec  27603  cnlnadjlem5  27717  shatomistici  28007  hatomistici  28008  nnindf  28375  ordtconlem1  28723  indf1ofs  28840  sigagenval  28955  ldsysgenld  28975  ldgenpisyslem1  28978  ldgenpisyslem2  28979  ldgenpisys  28981  ddemeas  29052  ismbfm  29067  imambfm  29077  dya2iocuni  29098  oms0  29118  omssubadd  29121  oms0OLD  29122  omssubaddOLD  29125  elcarsg  29130  issibf  29159  sitgfval  29167  oddpwdc  29180  eulerpartlemgh  29204  eulerpartlemgs2  29206  dstfrvel  29299  ballotlemfc0  29318  ballotlemfcc  29319  ballotlemiex  29327  ballotlemfrcn0  29355  ballotlemirc  29357  ballotlem7  29361  ballotlemiexOLD  29365  ballotlemfrcn0OLD  29393  ballotlemircOLD  29395  ballotlem7OLD  29399  conpcon  29951  iscvm  29975  cvmsi  29981  cvmsval  29982  cvmliftmolem2  29998  cvmliftiota  30017  snmlval  30047  elmpst  30167  elgiso  30307  sltval2  30536  sltres  30544  nodenselem7  30569  nofulllem5  30588  lineelsb2  30908  linerflx1  30909  fwddifval  30922  fwddifnval  30923  rankeq1o  30931  finminlem  30967  fneint  30997  fnessref  31006  topmeet  31013  topjoin  31014  neifg  31020  relowlssretop  31759  fin2solem  31924  fin2so  31925  poimirlem4  31937  poimirlem25  31958  poimirlem26  31959  poimirlem27  31960  poimirlem31  31964  poimirlem32  31965  opnmbllem0  31969  mblfinlem2  31971  itg2gt0cn  31990  indexa  32053  nninfnub  32073  istotbnd  32094  sstotbnd2  32099  isbnd  32105  isrngohom  32197  isrngoiso  32210  isidl  32240  ispridl  32260  ismaxidl  32266  prnc  32293  isfldidl  32294  islshp  32539  lssats  32572  islfl  32620  isat  32846  atlatmstc  32879  islln  33065  islpln  33089  islvol  33132  linepsubN  33311  elpmap  33317  pmapsub  33327  elpadd  33358  paddvaln0N  33360  islhp  33555  isldil  33669  isltrn  33678  isdilN  33714  istrnN  33717  diaval  34594  diaelval  34595  diaeldm  34598  diaelrnN  34607  cdlemm10N  34680  docaclN  34686  dibglbN  34728  dicval  34738  dicfnN  34745  dicvalrelN  34747  dihglblem2aN  34855  dihglblem2N  34856  dihglblem3N  34857  dih1dimatlem  34891  dihglb2  34904  dochvalr  34919  doch2val2  34926  dochocss  34928  islpolN  35045  mapd0  35227  isnacs  35540  elmzpcl  35562  mzpindd  35582  rencldnfilem  35657  irrapxlem6  35665  pellexlem3  35669  pellexlem5  35671  elpell1qr  35687  elpell14qr  35689  elpell1234qr  35691  pellfundre  35723  pellfundge  35724  pellfundlb  35726  pellfundglb  35727  rmspecnonsq  35749  jm2.22  35844  jm2.23  35845  rpnnen3lem  35880  fnwe2lem2  35903  fnwe2lem3  35904  elmnc  35989  dgraalem  36001  dgraalemOLD  36002  dgraaub  36007  dgraaubOLD  36008  mpaalem  36012  rgspnmin  36031  issdrg  36057  phisum  36070  nzss  36660  iccshift  37613  iooshift  37617  limcperiod  37702  sumnnodd  37704  ioodvbdlimc1lem1  37797  ioodvbdlimc1lem1OLD  37799  dvnprodlem1  37815  dvnprodlem3  37817  itgperiod  37852  stoweidlem14  37868  stoweidlem15  37869  stoweidlem16  37870  stoweidlem31  37886  stoweidlem36  37891  stoweidlem46  37901  stoweidlem48  37903  fourierdlem2  37965  fourierdlem3  37966  fourierdlem20  37983  fourierdlem25  37988  fourierdlem37  38001  fourierdlem42  38006  fourierdlem42OLD  38007  fourierdlem48  38012  fourierdlem51  38015  fourierdlem63  38027  fourierdlem64  38028  fourierdlem65  38029  fourierdlem79  38043  fourierdlem81  38045  elaa2lem  38091  elaa2lemOLD  38092  etransclem24  38117  etransclem26  38119  etransclem28  38121  etransclem35  38128  etransclem48OLD  38141  etransclem48  38142  salgenval  38176  salgenn0  38184  salgencl  38185  sssalgen  38188  salgenss  38189  salgenuni  38190  issalgend  38191  salgencntex  38196  sge0fodjrnlem  38252  meadjiunlem  38297  caragenel  38310  ovnlecvr  38374  ovnpnfelsup  38375  ovncvrrp  38380  ovnsubaddlem1  38386  hoidmv1lelem1  38407  hoidmv1lelem2  38408  hoidmv1lelem3  38409  hoidmvlelem1  38411  hoidmvlelem2  38412  hoidmvlelem4  38414  ovnhoilem1  38417  ovnlecvr2  38426  ovncvr2  38427  iccpart  38724  iseven  38751  isodd  38752  dfodd2  38760  dfeven5  38790  dfodd7  38791  upgrle  39168  umgredg2  39176  upgr1elem  39186  edgupgr  39211  edgumgr  39212  upgredg  39214  edgusgr  39234  usgruspgrb  39254  usgredg2ALT  39262  ushgredgedga  39292  ushgredgedgaloop  39294  subumgredg2  39340  subupgr  39342  upgrres1  39363  nbgrel  39393  nbupgrel  39396  nbumgrvtx  39397  nbusgreledg  39404  nbgrnself  39412  nbusgredgeu0  39425  nbusgrf1o0  39426  uvtxael  39443  uvtxael1  39451  uvtxusgrel  39459  umgr2v2e  39545  rgrusgrprc  39587  rgrx0ndm  39591  ismgmhm  39770  issubmgm  39776  rabsubmgmd  39778  mgmhmeql  39790  assintop  39832  isassintop  39833  assintopcllaw  39835  isrnghm  39879  isrngisom  39883  0even  39918  2even  39920  2zrngamgm  39926  dmatALTbasel  40182  lcoval  40192  elbigo  40349  secval  40454  cscval  40455  cotval  40456
  Copyright terms: Public domain W3C validator