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

Theorem elrab 3052
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 2540 . 2  |-  F/_ x A
2 nfcv 2540 . 2  |-  F/_ x B
3 nfv 1626 . 2  |-  F/ x ps
4 elrab.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
51, 2, 3, 4elrabf 3051 1  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1721   {crab 2670
This theorem is referenced by:  elrab3  3053  elrab2  3054  ralrab  3056  rexrab  3058  rabsnt  3841  unimax  4009  ssintub  4028  intminss  4036  reusv6OLD  4693  rabxfrd  4703  onnminsb  4743  dfom2  4806  ssnlim  4822  ssimaex  5747  weniso  6034  sorpsscmpl  6492  canth  6498  oeeulem  6803  nnawordex  6839  elpmg  6991  fineqvlem  7282  supub  7420  suplub  7421  ordtypelem6  7448  ordtypelem7  7449  hartogslem1  7467  hartogs  7469  wemapso2lem  7475  card2on  7478  elharval  7487  wdom2d  7504  cantnfs  7577  oemapvali  7596  rankuni2b  7735  scottex  7765  tskwe  7793  cardid2  7796  iscard2  7819  harval2  7840  cardmin2  7841  acni3  7884  alephsuc2  7917  kmlem1  7986  cofsmo  8105  coftr  8109  fin23lem11  8153  enfin2i  8157  fin1a2lem9  8244  fin1a2lem11  8246  axcc4  8275  axdc3lem2  8287  zorn2lem7  8338  ondomon  8394  alephval2  8403  grutsk  8653  pinq  8760  infm3  9923  infmrcl  9943  nnind  9974  peano2uz2  10313  peano5uzi  10314  dfuzi  10316  uzind  10317  uzind3  10319  uzind3OLD  10321  eluz1  10448  uzind4  10490  nnwos  10500  eqreznegel  10517  zsupss  10521  zmin  10526  elixx1  10881  elioo2  10913  elfz1  11004  flval3  11177  serge0  11332  expge0  11371  expge1  11372  hashbclem  11656  shftf  11849  rlimrege0  12328  incexc2  12573  divalglem4  12871  divalgmod  12881  bitsval  12891  bezout  12997  1nprm  13039  1idssfct  13040  isprm2  13042  phicl2  13112  hashdvds  13119  odzval  13132  odzcllem  13133  odzdvds  13136  pcpremul  13172  prmreclem1  13239  prmreclem2  13240  prmreclem3  13241  prmreclem5  13243  ramub  13336  rami  13338  ramub1lem1  13349  ramub1lem2  13350  ismre  13770  mrcflem  13786  mrcval  13790  ismri  13811  isacs  13831  isacs1i  13837  catlid  13863  catrid  13864  ismon  13914  isnat  14099  eldmcoa  14175  coaval  14178  ismhm  14695  issubm  14703  mhmeql  14719  gsumress  14732  gsumval2  14738  grplinv  14806  issubg  14899  cycsubg  14923  isnsg  14924  ghmeql  14983  isgim  15004  isga  15023  elcntz  15076  elcntzsn  15079  odid  15131  odlem2  15132  gexid  15170  gexlem2  15171  gexdvds  15173  isslw  15197  pgpssslw  15203  pj1id  15286  efgsfo  15326  oddvdssubg  15425  pgpfac1lem5  15592  ablfaclem2  15599  isirred  15759  issubrg  15823  isabv  15862  islss  15966  islmhm  16058  lmhmeql  16086  islmim  16089  islbs  16103  gsumbagdiaglem  16395  psrmulcllem  16406  psrlidm  16422  psrridm  16423  psrass1  16424  psrcom  16427  mplsubglem  16453  mpllsslem  16454  mplmonmul  16482  coe1mul2  16617  elocv  16850  isobs  16902  istopon  16945  fctop  17023  cctop  17025  ppttop  17026  pptbas  17027  epttop  17028  iscld  17046  clscld  17066  isnei  17122  neips  17132  neiptopnei  17151  iscn  17253  iscnp  17255  ordthauslem  17401  cmpsublem  17416  concompcon  17448  2ndc1stc  17467  2ndcdisj  17472  elkgen  17521  xkoopn  17574  xkoccn  17604  txdis1cn  17620  pthaus  17623  txkgen  17637  xkohaus  17638  xkococnlem  17644  xkococn  17645  xkoinjcn  17672  txcon  17674  elqtop  17682  nrmr0reg  17734  elmptrab  17812  fbssfi  17822  opnfbas  17827  elfg  17856  cfinfil  17878  csdfil  17879  supfil  17880  filssufilg  17896  uffix  17906  fixufil  17907  uffixfr  17908  uffixsn  17910  ufinffr  17914  ufilen  17915  elflim2  17949  supnfcls  18005  fclscf  18010  flimfnfcls  18013  alexsubALTlem2  18032  alexsubALTlem4  18034  alexsubALT  18035  ptcmplem2  18037  tmdgsum2  18079  symgtgp  18084  ghmcnp  18097  elutop  18216  isucn  18261  iscfilu  18271  ispsmet  18288  ismet  18306  isxmet  18307  elblps  18370  elbl  18371  restmetu  18570  icccmp  18809  elcncf  18872  ishtpy  18950  isphtpy  18959  om1elbas  19010  iscfil  19171  iscau  19182  iscmet  19190  lmle  19207  minveclem3  19283  minveclem4  19286  ovolshftlem1  19358  ovolscalem1  19362  ovolicc2lem3  19368  iundisj  19395  dyadmax  19443  dyadmbllem  19444  opnmbllem  19446  vitalilem2  19454  vitalilem3  19455  elcpn  19773  evlsval2  19894  ig1pval3  20050  coelem  20098  quotlem  20170  elqaalem1  20189  elqaalem3  20191  aannenlem1  20198  aannenlem2  20199  aalioulem2  20203  radcnv0  20285  dmarea  20749  jensen  20780  ftalem4  20811  ftalem5  20812  efnnfsumcl  20838  efchtdvds  20895  sqff1o  20918  dvdsdivcl  20919  fsumdvdsdiaglem  20921  dvdsppwf1o  20924  dvdsflf1o  20925  dvdsflsumcom  20926  musum  20929  muinv  20931  logfac2  20954  dchrelbas  20973  dchrfi  20992  lgsfle1  21042  lgsle1  21048  lgsdirprm  21066  lgsne0  21070  lgsquadlem1  21091  lgsquadlem2  21092  dchrvmasumlem1  21142  logsqvma  21189  pntleml  21258  umgrale  21309  umgra1  21314  uslgra1  21345  usgra1  21346  usgraedg2  21348  usgraedgrnv  21350  usgrarnedg  21357  usgraedg4  21359  usgraexmpl  21373  usgrares1  21377  nbgrael  21391  nbgraeledg  21395  nbgraf1olem3  21406  cusgrarn  21421  nbcusgra  21425  cusgrares  21434  uvtxel  21451  uvtxnbgra  21455  cusgrauvtxb  21458  eupath2  21655  umgrabi  21658  konigsberg  21662  grpoidinv2  21759  grpoinv  21768  isssp  22176  islno  22207  isblo  22236  ishmo  22265  ubthlem1  22325  ubthlem2  22326  htthlem  22373  ocel  22736  shsval2i  22842  ococin  22863  chsupsn  22868  eleigvec  23413  cnlnadjlem5  23527  shatomistici  23817  hatomistici  23818  indf1ofs  24376  sigagenval  24476  ismbfm  24555  imambfm  24565  dya2iocuni  24586  issibf  24601  sitgfval  24608  dstfrvel  24684  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemiex  24712  ballotlemfrcn0  24740  ballotlemirc  24742  ballotlem7  24746  conpcon  24875  iscvm  24899  cvmsi  24905  cvmsval  24906  cvmliftmolem2  24922  cvmliftiota  24941  snmlval  24971  elgiso  25060  sltval2  25524  sltres  25532  nodenselem7  25555  nofulllem5  25574  lineelsb2  25986  linerflx1  25987  rankeq1o  26016  mblfinlem  26143  itg2gt0cn  26159  finminlem  26211  fneint  26247  fnessref  26263  locfincmp  26274  topmeet  26283  topjoin  26284  neifg  26290  indexa  26325  nninfnub  26345  istotbnd  26368  sstotbnd2  26373  isbnd  26379  isrngohom  26471  isrngoiso  26484  isidl  26514  ispridl  26534  ismaxidl  26540  prnc  26567  isfldidl  26568  isnacs  26648  elmzpcl  26673  mzpindd  26693  rencldnfilem  26771  irrapxlem6  26780  pellexlem3  26784  pellexlem5  26786  elpell1qr  26800  elpell14qr  26802  elpell1234qr  26804  pellfundre  26834  pellfundge  26835  pellfundlb  26837  pellfundglb  26838  rmspecnonsq  26860  jm2.22  26956  jm2.23  26957  rpnnen3lem  26992  fnwe2lem2  27016  fnwe2lem3  27017  dsmmelbas  27073  frlmelbas  27092  frlmssuvc2  27115  islinds  27147  elmnc  27209  dgraalem  27218  dgraaub  27221  mpaalem  27225  rgspnmin  27244  issubmd  27251  pmtrval  27262  pmtrrn  27267  symgsssg  27276  symgfisg  27277  psgnunilem5  27285  issdrg  27373  phisum  27386  stoweidlem14  27630  stoweidlem15  27631  stoweidlem16  27632  stoweidlem31  27647  stoweidlem36  27652  stoweidlem46  27662  stoweidlem48  27664  el2wlkonot  28066  el2spthonot  28067  el2spthonot0  28068  el2wlksoton  28075  el2spthsoton  28076  el2wlksotot  28079  2spotdisj  28164  usg2spot2nb  28168  usgreg2spot  28170  secval  28204  cscval  28205  cotval  28206  islshp  29462  lssats  29495  islfl  29543  isat  29769  atlatmstc  29802  islln  29988  islpln  30012  islvol  30055  linepsubN  30234  elpmap  30240  pmapsub  30250  elpadd  30281  paddvaln0N  30283  islhp  30478  isldil  30592  isltrn  30601  isdilN  30636  istrnN  30639  diaval  31515  diaelval  31516  diaeldm  31519  diaelrnN  31528  cdlemm10N  31601  docaclN  31607  dibglbN  31649  dicval  31659  dicfnN  31666  dicvalrelN  31668  dihglblem2aN  31776  dihglblem2N  31777  dihglblem3N  31778  dih1dimatlem  31812  dihglb2  31825  dochvalr  31840  doch2val2  31847  dochocss  31849  islpolN  31966  mapd0  32148
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918
  Copyright terms: Public domain W3C validator