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

Theorem elrab 3084
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 2571 . 2  |-  F/_ x A
2 nfcv 2571 . 2  |-  F/_ x B
3 nfv 1629 . 2  |-  F/ x ps
4 elrab.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
51, 2, 3, 4elrabf 3083 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 1652    e. wcel 1725   {crab 2701
This theorem is referenced by:  elrab3  3085  elrab2  3086  ralrab  3088  rexrab  3090  rabsnt  3873  unimax  4041  ssintub  4060  intminss  4068  reusv6OLD  4725  rabxfrd  4735  onnminsb  4775  dfom2  4838  ssnlim  4854  ssimaex  5779  weniso  6066  sorpsscmpl  6524  canth  6530  oeeulem  6835  nnawordex  6871  elpmg  7023  fineqvlem  7314  supub  7453  suplub  7454  ordtypelem6  7481  ordtypelem7  7482  hartogslem1  7500  hartogs  7502  wemapso2lem  7508  card2on  7511  elharval  7520  wdom2d  7537  cantnfs  7610  oemapvali  7629  rankuni2b  7768  scottex  7798  tskwe  7826  cardid2  7829  iscard2  7852  harval2  7873  cardmin2  7874  acni3  7917  alephsuc2  7950  kmlem1  8019  cofsmo  8138  coftr  8142  fin23lem11  8186  enfin2i  8190  fin1a2lem9  8277  fin1a2lem11  8279  axcc4  8308  axdc3lem2  8320  zorn2lem7  8371  ondomon  8427  alephval2  8436  grutsk  8686  pinq  8793  infm3  9956  infmrcl  9976  nnind  10007  peano2uz2  10346  peano5uzi  10347  dfuzi  10349  uzind  10350  uzind3  10352  uzind3OLD  10354  eluz1  10481  uzind4  10523  nnwos  10533  eqreznegel  10550  zsupss  10554  zmin  10559  elixx1  10914  elioo2  10946  elfz1  11037  flval3  11210  serge0  11365  expge0  11404  expge1  11405  hashbclem  11689  shftf  11882  rlimrege0  12361  incexc2  12606  divalglem4  12904  divalgmod  12914  bitsval  12924  bezout  13030  1nprm  13072  1idssfct  13073  isprm2  13075  phicl2  13145  hashdvds  13152  odzval  13165  odzcllem  13166  odzdvds  13169  pcpremul  13205  prmreclem1  13272  prmreclem2  13273  prmreclem3  13274  prmreclem5  13276  ramub  13369  rami  13371  ramub1lem1  13382  ramub1lem2  13383  ismre  13803  mrcflem  13819  mrcval  13823  ismri  13844  isacs  13864  isacs1i  13870  catlid  13896  catrid  13897  ismon  13947  isnat  14132  eldmcoa  14208  coaval  14211  ismhm  14728  issubm  14736  mhmeql  14752  gsumress  14765  gsumval2  14771  grplinv  14839  issubg  14932  cycsubg  14956  isnsg  14957  ghmeql  15016  isgim  15037  isga  15056  elcntz  15109  elcntzsn  15112  odid  15164  odlem2  15165  gexid  15203  gexlem2  15204  gexdvds  15206  isslw  15230  pgpssslw  15236  pj1id  15319  efgsfo  15359  oddvdssubg  15458  pgpfac1lem5  15625  ablfaclem2  15632  isirred  15792  issubrg  15856  isabv  15895  islss  15999  islmhm  16091  lmhmeql  16119  islmim  16122  islbs  16136  gsumbagdiaglem  16428  psrmulcllem  16439  psrlidm  16455  psrridm  16456  psrass1  16457  psrcom  16460  mplsubglem  16486  mpllsslem  16487  mplmonmul  16515  coe1mul2  16650  elocv  16883  isobs  16935  istopon  16978  fctop  17056  cctop  17058  ppttop  17059  pptbas  17060  epttop  17061  iscld  17079  clscld  17099  isnei  17155  neips  17165  neiptopnei  17184  iscn  17287  iscnp  17289  ordthauslem  17435  cmpsublem  17450  concompcon  17483  2ndc1stc  17502  2ndcdisj  17507  elkgen  17556  xkoopn  17609  xkoccn  17639  txdis1cn  17655  pthaus  17658  txkgen  17672  xkohaus  17673  xkococnlem  17679  xkococn  17680  xkoinjcn  17707  txcon  17709  elqtop  17717  nrmr0reg  17769  elmptrab  17847  fbssfi  17857  opnfbas  17862  elfg  17891  cfinfil  17913  csdfil  17914  supfil  17915  filssufilg  17931  uffix  17941  fixufil  17942  uffixfr  17943  uffixsn  17945  ufinffr  17949  ufilen  17950  elflim2  17984  supnfcls  18040  fclscf  18045  flimfnfcls  18048  alexsubALTlem2  18067  alexsubALTlem4  18069  alexsubALT  18070  ptcmplem2  18072  tmdgsum2  18114  symgtgp  18119  ghmcnp  18132  elutop  18251  isucn  18296  iscfilu  18306  ispsmet  18323  ismet  18341  isxmet  18342  elblps  18405  elbl  18406  restmetu  18605  icccmp  18844  elcncf  18907  ishtpy  18985  isphtpy  18994  om1elbas  19045  iscfil  19206  iscau  19217  iscmet  19225  lmle  19242  minveclem3  19318  minveclem4  19321  ovolshftlem1  19393  ovolscalem1  19397  ovolicc2lem3  19403  iundisj  19430  dyadmax  19478  dyadmbllem  19479  opnmbllem  19481  vitalilem2  19489  vitalilem3  19490  elcpn  19808  evlsval2  19929  ig1pval3  20085  coelem  20133  quotlem  20205  elqaalem1  20224  elqaalem3  20226  aannenlem1  20233  aannenlem2  20234  aalioulem2  20238  radcnv0  20320  dmarea  20784  jensen  20815  ftalem4  20846  ftalem5  20847  efnnfsumcl  20873  efchtdvds  20930  sqff1o  20953  dvdsdivcl  20954  fsumdvdsdiaglem  20956  dvdsppwf1o  20959  dvdsflf1o  20960  dvdsflsumcom  20961  musum  20964  muinv  20966  logfac2  20989  dchrelbas  21008  dchrfi  21027  lgsfle1  21077  lgsle1  21083  lgsdirprm  21101  lgsne0  21105  lgsquadlem1  21126  lgsquadlem2  21127  dchrvmasumlem1  21177  logsqvma  21224  pntleml  21293  umgrale  21344  umgra1  21349  uslgra1  21380  usgra1  21381  usgraedg2  21383  usgraedgrnv  21385  usgrarnedg  21392  usgraedg4  21394  usgraexmpl  21408  usgrares1  21412  nbgrael  21426  nbgraeledg  21430  nbgraf1olem3  21441  cusgrarn  21456  nbcusgra  21460  cusgrares  21469  uvtxel  21486  uvtxnbgra  21490  cusgrauvtxb  21493  eupath2  21690  umgrabi  21693  konigsberg  21697  grpoidinv2  21794  grpoinv  21803  isssp  22211  islno  22242  isblo  22271  ishmo  22300  ubthlem1  22360  ubthlem2  22361  htthlem  22408  ocel  22771  shsval2i  22877  ococin  22898  chsupsn  22903  eleigvec  23448  cnlnadjlem5  23562  shatomistici  23852  hatomistici  23853  indf1ofs  24411  sigagenval  24511  ismbfm  24590  imambfm  24600  dya2iocuni  24621  issibf  24636  sitgfval  24643  dstfrvel  24719  ballotlemfc0  24738  ballotlemfcc  24739  ballotlemiex  24747  ballotlemfrcn0  24775  ballotlemirc  24777  ballotlem7  24781  conpcon  24910  iscvm  24934  cvmsi  24940  cvmsval  24941  cvmliftmolem2  24957  cvmliftiota  24976  snmlval  25006  elgiso  25095  sltval2  25565  sltres  25573  nodenselem7  25596  nofulllem5  25615  lineelsb2  26030  linerflx1  26031  rankeq1o  26060  mblfinlem  26190  itg2gt0cn  26206  finminlem  26258  fneint  26294  fnessref  26310  locfincmp  26321  topmeet  26330  topjoin  26331  neifg  26337  indexa  26372  nninfnub  26392  istotbnd  26415  sstotbnd2  26420  isbnd  26426  isrngohom  26518  isrngoiso  26531  isidl  26561  ispridl  26581  ismaxidl  26587  prnc  26614  isfldidl  26615  isnacs  26695  elmzpcl  26720  mzpindd  26740  rencldnfilem  26818  irrapxlem6  26827  pellexlem3  26831  pellexlem5  26833  elpell1qr  26847  elpell14qr  26849  elpell1234qr  26851  pellfundre  26881  pellfundge  26882  pellfundlb  26884  pellfundglb  26885  rmspecnonsq  26907  jm2.22  27003  jm2.23  27004  rpnnen3lem  27039  fnwe2lem2  27063  fnwe2lem3  27064  dsmmelbas  27120  frlmelbas  27139  frlmssuvc2  27162  islinds  27194  elmnc  27256  dgraalem  27265  dgraaub  27268  mpaalem  27272  rgspnmin  27291  issubmd  27298  pmtrval  27309  pmtrrn  27314  symgsssg  27323  symgfisg  27324  psgnunilem5  27332  issdrg  27420  phisum  27433  stoweidlem14  27677  stoweidlem15  27678  stoweidlem16  27679  stoweidlem31  27694  stoweidlem36  27699  stoweidlem46  27709  stoweidlem48  27711  el2wlkonot  28210  el2spthonot  28211  el2spthonot0  28212  el2wlksoton  28219  el2spthsoton  28220  el2wlksotot  28223  2spotdisj  28308  usg2spot2nb  28312  usgreg2spot  28314  secval  28348  cscval  28349  cotval  28350  islshp  29616  lssats  29649  islfl  29697  isat  29923  atlatmstc  29956  islln  30142  islpln  30166  islvol  30209  linepsubN  30388  elpmap  30394  pmapsub  30404  elpadd  30435  paddvaln0N  30437  islhp  30632  isldil  30746  isltrn  30755  isdilN  30790  istrnN  30793  diaval  31669  diaelval  31670  diaeldm  31673  diaelrnN  31682  cdlemm10N  31755  docaclN  31761  dibglbN  31803  dicval  31813  dicfnN  31820  dicvalrelN  31822  dihglblem2aN  31930  dihglblem2N  31931  dihglblem3N  31932  dih1dimatlem  31966  dihglb2  31979  dochvalr  31994  doch2val2  32001  dochocss  32003  islpolN  32120  mapd0  32302
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950
  Copyright terms: Public domain W3C validator