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

Theorem elrab 2936
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 2432 . 2  |-  F/_ x A
2 nfcv 2432 . 2  |-  F/_ x B
3 nfv 1609 . 2  |-  F/ x ps
4 elrab.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
51, 2, 3, 4elrabf 2935 1  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1632    e. wcel 1696   {crab 2560
This theorem is referenced by:  elrab3  2937  elrab2  2938  ralrab  2940  rexrab  2942  rabsnt  3717  unimax  3877  ssintub  3896  intminss  3904  reusv6OLD  4561  rabxfrd  4571  onnminsb  4611  dfom2  4674  ssnlim  4690  ssimaex  5600  weniso  5868  sorpsscmpl  6304  canth  6310  oeeulem  6615  nnawordex  6651  elpmg  6802  fineqvlem  7093  supub  7226  suplub  7227  ordtypelem6  7254  ordtypelem7  7255  hartogslem1  7273  hartogs  7275  wemapso2lem  7281  card2on  7284  elharval  7293  wdom2d  7310  cantnfs  7383  oemapvali  7402  rankuni2b  7541  scottex  7571  tskwe  7599  cardid2  7602  iscard2  7625  harval2  7646  cardmin2  7647  acni3  7690  alephsuc2  7723  kmlem1  7792  cofsmo  7911  coftr  7915  fin23lem11  7959  enfin2i  7963  fin1a2lem9  8050  fin1a2lem11  8052  axcc4  8081  axdc3lem2  8093  zorn2lem7  8145  ondomon  8201  alephval2  8210  grutsk  8460  pinq  8567  infm3  9729  infmrcl  9749  nnind  9780  peano2uz2  10115  peano5uzi  10116  dfuzi  10118  uzind  10119  uzind3  10121  uzind3OLD  10123  eluz1  10250  uzind4  10292  nnwos  10302  eqreznegel  10319  supminf  10321  zsupss  10323  zmin  10328  elixx1  10681  elioo2  10713  elfz1  10803  flval3  10961  serge0  11116  expge0  11154  expge1  11155  hashbclem  11406  shftf  11590  rlimrege0  12069  incexc2  12313  divalglem4  12611  divalgmod  12621  bitsval  12631  sadval  12663  smuval  12688  bezout  12737  1nprm  12779  1idssfct  12780  isprm2  12782  phicl2  12852  hashdvds  12859  odzval  12872  odzcllem  12873  odzdvds  12876  pcpremul  12912  prmreclem1  12979  prmreclem2  12980  prmreclem3  12981  prmreclem5  12983  ramub  13076  rami  13078  ramub1lem1  13089  ramub1lem2  13090  ismre  13508  mrcflem  13524  mrcval  13528  ismri  13549  isacs  13569  isacs1i  13575  catlid  13601  catrid  13602  ismon  13652  isnat  13837  eldmcoa  13913  coaval  13916  ismhm  14433  issubm  14441  mhmeql  14457  gsumress  14470  gsumval2  14476  grplinv  14544  issubg  14637  cycsubg  14661  isnsg  14662  ghmeql  14721  isgim  14742  isga  14761  elcntz  14814  elcntzsn  14817  odid  14869  odlem2  14870  gexid  14908  gexlem2  14909  gexdvds  14911  isslw  14935  pgpssslw  14941  pj1id  15024  efgsfo  15064  oddvdssubg  15163  pgpfac1lem5  15330  ablfaclem2  15337  isirred  15497  issubrg  15561  isabv  15600  islss  15708  islmhm  15800  lmhmeql  15828  islmim  15831  islbs  15845  gsumbagdiaglem  16137  psrmulcllem  16148  psrlidm  16164  psrridm  16165  psrass1  16166  psrcom  16169  mplsubglem  16195  mpllsslem  16196  mplmonmul  16224  coe1mul2  16362  elocv  16584  isobs  16636  istopon  16679  fctop  16757  cctop  16759  ppttop  16760  pptbas  16761  epttop  16762  iscld  16780  clscld  16800  isnei  16856  neips  16866  iscn  16981  iscnp  16983  ordthauslem  17127  cmpsublem  17142  concompcon  17174  2ndc1stc  17193  2ndcdisj  17198  elkgen  17247  xkoopn  17300  xkoccn  17329  txdis1cn  17345  pthaus  17348  txkgen  17362  xkohaus  17363  xkococnlem  17369  xkococn  17370  xkoinjcn  17397  txcon  17399  elqtop  17404  nrmr0reg  17456  elmptrab  17538  fbssfi  17548  opnfbas  17553  elfg  17582  cfinfil  17604  csdfil  17605  supfil  17606  filssufilg  17622  uffix  17632  fixufil  17633  uffixfr  17634  uffixsn  17636  ufinffr  17640  ufilen  17641  elflim2  17675  supnfcls  17731  fclscf  17736  flimfnfcls  17739  alexsubALTlem2  17758  alexsubALTlem4  17760  alexsubALT  17761  ptcmplem2  17763  tmdgsum2  17795  symgtgp  17800  ghmcnp  17813  ismet  17904  isxmet  17905  elbl  17965  icccmp  18346  elcncf  18409  ishtpy  18486  isphtpy  18495  om1elbas  18546  iscfil  18707  iscau  18718  iscmet  18726  lmle  18743  minveclem3  18809  minveclem4  18812  ovolshftlem1  18884  ovolscalem1  18888  ovolicc2lem3  18894  iundisj  18921  dyadmax  18969  dyadmbllem  18970  opnmbllem  18972  vitalilem2  18980  vitalilem3  18981  elcpn  19299  evlsval2  19420  ig1pval3  19576  coelem  19624  quotlem  19696  elqaalem1  19715  elqaalem3  19717  aannenlem1  19724  aannenlem2  19725  aalioulem2  19729  radcnv0  19808  dmarea  20268  jensen  20299  ftalem4  20329  ftalem5  20330  efnnfsumcl  20356  efchtdvds  20413  sqff1o  20436  dvdsdivcl  20437  fsumdvdsdiaglem  20439  dvdsppwf1o  20442  dvdsflf1o  20443  dvdsflsumcom  20444  musum  20447  muinv  20449  logfac2  20472  dchrelbas  20491  dchrfi  20510  lgsfle1  20560  lgsle1  20566  lgsdirprm  20584  lgsne0  20588  lgsquadlem1  20609  lgsquadlem2  20610  dchrvmasumlem1  20660  logsqvma  20707  pntleml  20776  grpoidinv2  20901  grpoinv  20910  isssp  21316  islno  21347  isblo  21376  ishmo  21405  ubthlem1  21465  ubthlem2  21466  htthlem  21513  ocel  21876  shsval2i  21982  ococin  22003  chsupsn  22008  eleigvec  22553  cnlnadjlem5  22667  shatomistici  22957  hatomistici  22958  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemiex  23076  ballotlemfrcn0  23104  ballotlemirc  23106  ballotlem7  23110  sigagenval  23516  sigagenss  23525  ismbfm  23572  imambfm  23582  indf1ofs  23624  dstfrvel  23689  conpcon  23781  iscvm  23805  cvmsi  23811  cvmsval  23812  cvmliftmolem2  23828  cvmliftiota  23847  umgrale  23888  umgra1  23893  eupath2  23919  umgrabi  23922  konigsberg  23926  snmlval  23929  elgiso  24018  sltval2  24381  sltres  24389  nodenselem7  24412  nofulllem5  24431  lineelsb2  24843  linerflx1  24844  rankeq1o  24873  itg2gt0cn  25006  dstr  25274  puub2  25361  puub  25362  supdef  25365  ismxl2  25370  ismnl2  25371  isidlNEW  25549  usptoplem  25649  usptop  25653  prcnt  25654  fgsb2  25658  iint  25715  ishomc  25892  ismonb  25913  isepib  25923  cinvlem3  25933  isfunb  25938  issrc  25970  propsrc  25971  isntr  25976  islimcat  25979  isnword  26089  isconcl2b  26201  isibcg  26294  finminlem  26334  fneint  26380  fnessref  26396  locfincmp  26407  topmeet  26416  topjoin  26417  neifg  26423  indexa  26515  nninfnub  26564  istotbnd  26596  sstotbnd2  26601  isbnd  26607  isrngohom  26699  isrngoiso  26712  isidl  26742  ispridl  26762  ismaxidl  26768  prnc  26795  isfldidl  26796  isnacs  26882  elmzpcl  26907  mzpindd  26927  rencldnfilem  27006  irrapxlem6  27015  pellexlem3  27019  pellexlem5  27021  elpell1qr  27035  elpell14qr  27037  elpell1234qr  27039  pellfundre  27069  pellfundge  27070  pellfundlb  27072  pellfundglb  27073  rmspecnonsq  27095  jm2.22  27191  jm2.23  27192  rpnnen3lem  27227  fnwe2lem2  27251  fnwe2lem3  27252  dsmmelbas  27308  frlmelbas  27327  frlmssuvc2  27350  islinds  27382  elmnc  27444  dgraalem  27453  dgraaub  27456  mpaalem  27460  rgspnmin  27479  issubmd  27486  pmtrval  27497  pmtrrn  27502  symgsssg  27511  symgfisg  27512  psgnunilem5  27520  issdrg  27608  phisum  27621  stoweidlem14  27866  stoweidlem15  27867  stoweidlem31  27883  stoweidlem36  27888  stoweidlem37  27889  stoweidlem46  27898  stoweidlem48  27900  stoweidlem51  27903  uslgra1  28252  usgra1  28253  usgraedg2  28255  usgraedgrnv  28257  usgraexmpl  28267  nbgrael  28275  nbgraeledg  28279  nbcusgra  28298  uvtxel  28302  uvtxisvtx  28303  uvtxnbgra  28306  cusgrauvtx  28309  secval  28471  cscval  28472  cotval  28473  islshp  29791  lssats  29824  islfl  29872  isat  30098  atlatmstc  30131  islln  30317  islpln  30341  islvol  30384  linepsubN  30563  elpmap  30569  pmapsub  30579  elpadd  30610  paddvaln0N  30612  islhp  30807  isldil  30921  isltrn  30930  isdilN  30965  istrnN  30968  diaval  31844  diaelval  31845  diaeldm  31848  diaelrnN  31857  cdlemm10N  31930  docaclN  31936  dibglbN  31978  dicval  31988  dicfnN  31995  dicvalrelN  31997  dihglblem2aN  32105  dihglblem2N  32106  dihglblem3N  32107  dih1dimatlem  32141  dihglb2  32154  dochvalr  32169  doch2val2  32176  dochocss  32178  islpolN  32295  mapd0  32477
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803
  Copyright terms: Public domain W3C validator