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

Theorem elrab 3094
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 2574 . 2  |-  F/_ x A
2 nfcv 2574 . 2  |-  F/_ x B
3 nfv 1630 . 2  |-  F/ x ps
4 elrab.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
51, 2, 3, 4elrabf 3093 1  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653    e. wcel 1726   {crab 2711
This theorem is referenced by:  elrab3  3095  elrab2  3096  ralrab  3098  rexrab  3100  rabsnt  3883  unimax  4051  ssintub  4070  intminss  4078  reusv6OLD  4737  rabxfrd  4747  onnminsb  4787  dfom2  4850  ssnlim  4866  ssimaex  5791  weniso  6078  sorpsscmpl  6536  canth  6542  oeeulem  6847  nnawordex  6883  elpmg  7035  fineqvlem  7326  supub  7467  suplub  7468  ordtypelem6  7495  ordtypelem7  7496  hartogslem1  7514  hartogs  7516  wemapso2lem  7522  card2on  7525  elharval  7534  wdom2d  7551  cantnfs  7624  oemapvali  7643  rankuni2b  7782  scottex  7814  tskwe  7842  cardid2  7845  iscard2  7868  harval2  7889  cardmin2  7890  acni3  7933  alephsuc2  7966  kmlem1  8035  cofsmo  8154  coftr  8158  fin23lem11  8202  enfin2i  8206  fin1a2lem9  8293  fin1a2lem11  8295  axcc4  8324  axdc3lem2  8336  zorn2lem7  8387  ondomon  8443  alephval2  8452  grutsk  8702  pinq  8809  infm3  9972  infmrcl  9992  nnind  10023  peano2uz2  10362  peano5uzi  10363  dfuzi  10365  uzind  10366  uzind3  10368  uzind3OLD  10370  eluz1  10497  uzind4  10539  nnwos  10549  eqreznegel  10566  zsupss  10570  zmin  10575  elixx1  10930  elioo2  10962  elfz1  11053  flval3  11227  serge0  11382  expge0  11421  expge1  11422  hashbclem  11706  shftf  11899  rlimrege0  12378  incexc2  12623  divalglem4  12921  divalgmod  12931  bitsval  12941  bezout  13047  1nprm  13089  1idssfct  13090  isprm2  13092  phicl2  13162  hashdvds  13169  odzval  13182  odzcllem  13183  odzdvds  13186  pcpremul  13222  prmreclem1  13289  prmreclem2  13290  prmreclem3  13291  prmreclem5  13293  ramub  13386  rami  13388  ramub1lem1  13399  ramub1lem2  13400  ismre  13820  mrcflem  13836  mrcval  13840  ismri  13861  isacs  13881  isacs1i  13887  catlid  13913  catrid  13914  ismon  13964  isnat  14149  eldmcoa  14225  coaval  14228  ismhm  14745  issubm  14753  mhmeql  14769  gsumress  14782  gsumval2  14788  grplinv  14856  issubg  14949  cycsubg  14973  isnsg  14974  ghmeql  15033  isgim  15054  isga  15073  elcntz  15126  elcntzsn  15129  odid  15181  odlem2  15182  gexid  15220  gexlem2  15221  gexdvds  15223  isslw  15247  pgpssslw  15253  pj1id  15336  efgsfo  15376  oddvdssubg  15475  pgpfac1lem5  15642  ablfaclem2  15649  isirred  15809  issubrg  15873  isabv  15912  islss  16016  islmhm  16108  lmhmeql  16136  islmim  16139  islbs  16153  gsumbagdiaglem  16445  psrmulcllem  16456  psrlidm  16472  psrridm  16473  psrass1  16474  psrcom  16477  mplsubglem  16503  mpllsslem  16504  mplmonmul  16532  coe1mul2  16667  elocv  16900  isobs  16952  istopon  16995  fctop  17073  cctop  17075  ppttop  17076  pptbas  17077  epttop  17078  iscld  17096  clscld  17116  isnei  17172  neips  17182  neiptopnei  17201  iscn  17304  iscnp  17306  ordthauslem  17452  cmpsublem  17467  concompcon  17500  2ndc1stc  17519  2ndcdisj  17524  elkgen  17573  xkoopn  17626  xkoccn  17656  txdis1cn  17672  pthaus  17675  txkgen  17689  xkohaus  17690  xkococnlem  17696  xkococn  17697  xkoinjcn  17724  txcon  17726  elqtop  17734  nrmr0reg  17786  elmptrab  17864  fbssfi  17874  opnfbas  17879  elfg  17908  cfinfil  17930  csdfil  17931  supfil  17932  filssufilg  17948  uffix  17958  fixufil  17959  uffixfr  17960  uffixsn  17962  ufinffr  17966  ufilen  17967  elflim2  18001  supnfcls  18057  fclscf  18062  flimfnfcls  18065  alexsubALTlem2  18084  alexsubALTlem4  18086  alexsubALT  18087  ptcmplem2  18089  tmdgsum2  18131  symgtgp  18136  ghmcnp  18149  elutop  18268  isucn  18313  iscfilu  18323  ispsmet  18340  ismet  18358  isxmet  18359  elblps  18422  elbl  18423  restmetu  18622  icccmp  18861  elcncf  18924  ishtpy  19002  isphtpy  19011  om1elbas  19062  iscfil  19223  iscau  19234  iscmet  19242  lmle  19259  minveclem3  19335  minveclem4  19338  ovolshftlem1  19410  ovolscalem1  19414  ovolicc2lem3  19420  iundisj  19447  dyadmax  19495  dyadmbllem  19496  opnmbllem  19498  vitalilem2  19506  vitalilem3  19507  elcpn  19825  evlsval2  19946  ig1pval3  20102  coelem  20150  quotlem  20222  elqaalem1  20241  elqaalem3  20243  aannenlem1  20250  aannenlem2  20251  aalioulem2  20255  radcnv0  20337  dmarea  20801  jensen  20832  ftalem4  20863  ftalem5  20864  efnnfsumcl  20890  efchtdvds  20947  sqff1o  20970  dvdsdivcl  20971  fsumdvdsdiaglem  20973  dvdsppwf1o  20976  dvdsflf1o  20977  dvdsflsumcom  20978  musum  20981  muinv  20983  logfac2  21006  dchrelbas  21025  dchrfi  21044  lgsfle1  21094  lgsle1  21100  lgsdirprm  21118  lgsne0  21122  lgsquadlem1  21143  lgsquadlem2  21144  dchrvmasumlem1  21194  logsqvma  21241  pntleml  21310  umgrale  21361  umgra1  21366  uslgra1  21397  usgra1  21398  usgraedg2  21400  usgraedgrnv  21402  usgrarnedg  21409  usgraedg4  21411  usgraexmpl  21425  usgrares1  21429  nbgrael  21443  nbgraeledg  21447  nbgraf1olem3  21458  cusgrarn  21473  nbcusgra  21477  cusgrares  21486  uvtxel  21503  uvtxnbgra  21507  cusgrauvtxb  21510  eupath2  21707  umgrabi  21710  konigsberg  21714  grpoidinv2  21811  grpoinv  21820  isssp  22228  islno  22259  isblo  22288  ishmo  22317  ubthlem1  22377  ubthlem2  22378  htthlem  22425  ocel  22788  shsval2i  22894  ococin  22915  chsupsn  22920  eleigvec  23465  cnlnadjlem5  23579  shatomistici  23869  hatomistici  23870  indf1ofs  24428  sigagenval  24528  ismbfm  24607  imambfm  24617  dya2iocuni  24638  issibf  24653  sitgfval  24660  dstfrvel  24736  ballotlemfc0  24755  ballotlemfcc  24756  ballotlemiex  24764  ballotlemfrcn0  24792  ballotlemirc  24794  ballotlem7  24798  conpcon  24927  iscvm  24951  cvmsi  24957  cvmsval  24958  cvmliftmolem2  24974  cvmliftiota  24993  snmlval  25023  elgiso  25112  sltval2  25616  sltres  25624  nodenselem7  25647  nofulllem5  25666  lineelsb2  26087  linerflx1  26088  rankeq1o  26117  opnmbllem0  26254  mblfinlem2  26256  itg2gt0cn  26274  finminlem  26335  fneint  26371  fnessref  26387  locfincmp  26398  topmeet  26407  topjoin  26408  neifg  26414  indexa  26449  nninfnub  26469  istotbnd  26492  sstotbnd2  26497  isbnd  26503  isrngohom  26595  isrngoiso  26608  isidl  26638  ispridl  26658  ismaxidl  26664  prnc  26691  isfldidl  26692  isnacs  26772  elmzpcl  26797  mzpindd  26817  rencldnfilem  26895  irrapxlem6  26904  pellexlem3  26908  pellexlem5  26910  elpell1qr  26924  elpell14qr  26926  elpell1234qr  26928  pellfundre  26958  pellfundge  26959  pellfundlb  26961  pellfundglb  26962  rmspecnonsq  26984  jm2.22  27080  jm2.23  27081  rpnnen3lem  27116  fnwe2lem2  27140  fnwe2lem3  27141  dsmmelbas  27196  frlmelbas  27215  frlmssuvc2  27238  islinds  27270  elmnc  27332  dgraalem  27341  dgraaub  27344  mpaalem  27348  rgspnmin  27367  issubmd  27374  pmtrval  27385  pmtrrn  27390  symgsssg  27399  symgfisg  27400  psgnunilem5  27408  issdrg  27496  phisum  27509  stoweidlem14  27753  stoweidlem15  27754  stoweidlem16  27755  stoweidlem31  27770  stoweidlem36  27775  stoweidlem46  27785  stoweidlem48  27787  elss2pr  28195  iswwlk  28365  iswwlkn  28366  el2wlkonot  28401  el2spthonot  28402  el2spthonot0  28403  el2wlksoton  28410  el2spthsoton  28411  el2wlksotot  28414  2spotdisj  28524  usg2spot2nb  28528  usgreg2spot  28530  secval  28564  cscval  28565  cotval  28566  islshp  29851  lssats  29884  islfl  29932  isat  30158  atlatmstc  30191  islln  30377  islpln  30401  islvol  30444  linepsubN  30623  elpmap  30629  pmapsub  30639  elpadd  30670  paddvaln0N  30672  islhp  30867  isldil  30981  isltrn  30990  isdilN  31025  istrnN  31028  diaval  31904  diaelval  31905  diaeldm  31908  diaelrnN  31917  cdlemm10N  31990  docaclN  31996  dibglbN  32038  dicval  32048  dicfnN  32055  dicvalrelN  32057  dihglblem2aN  32165  dihglblem2N  32166  dihglblem3N  32167  dih1dimatlem  32201  dihglb2  32214  dochvalr  32229  doch2val2  32236  dochocss  32238  islpolN  32355  mapd0  32537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960
  Copyright terms: Public domain W3C validator