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

Theorem elrab 3112
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 1673 . 2  |-  F/ x ps
4 elrab.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
51, 2, 3, 4elrabf 3110 1  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369    e. wcel 1756   {crab 2714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-v 2969
This theorem is referenced by:  elrab3  3113  elrab2  3114  ralrab  3116  rexrab  3118  rabsnt  3947  unimax  4122  ssintub  4141  intminss  4149  reusv6OLD  4498  rabxfrd  4508  ssimaex  5751  weniso  6040  canth  6044  sorpsscmpl  6366  onnminsb  6410  dfom2  6473  ssnlim  6489  elsuppfn  6693  ressuppssdif  6705  oeeulem  7032  nnawordex  7068  elpmg  7220  fineqvlem  7519  mapfienlem2  7647  supub  7701  suplub  7702  ordtypelem6  7729  ordtypelem7  7730  hartogslem1  7748  hartogs  7750  wemapsolem  7756  card2on  7761  elharval  7770  wdom2d  7787  cantnfs  7866  oemapvali  7884  cantnfsOLD  7896  rankuni2b  8052  scottex  8084  tskwe  8112  cardid2  8115  iscard2  8138  harval2  8159  cardmin2  8160  acni3  8209  alephsuc2  8242  kmlem1  8311  cofsmo  8430  coftr  8434  fin23lem11  8478  enfin2i  8482  fin1a2lem9  8569  fin1a2lem11  8571  axcc4  8600  axdc3lem2  8612  zorn2lem7  8663  ondomon  8719  alephval2  8728  grutsk  8981  pinq  9088  infm3  10281  infmrcl  10301  nnind  10332  peano2uz2  10721  peano5uzi  10722  dfuzi  10724  uzind  10725  uzind3  10727  uzind3OLD  10729  eluz1  10857  uzind4  10904  nnwos  10914  eqreznegel  10932  zsupss  10936  zmin  10941  elixx1  11301  elioo2  11333  elfz1  11434  flval3  11655  serge0  11852  expge0  11892  expge1  11893  pr2pwpr  12175  hashbclem  12197  disjxwrd  12341  shftf  12560  rlimrege0  13049  incexc2  13293  divalglem4  13592  divalgmod  13602  bitsval  13612  bezout  13718  1nprm  13760  1idssfct  13761  isprm2  13763  phicl2  13835  hashdvds  13842  odzval  13855  odzcllem  13856  odzdvds  13859  pcpremul  13902  prmreclem1  13969  prmreclem2  13970  prmreclem3  13971  prmreclem5  13973  ramub  14066  rami  14068  ramub1lem1  14079  ramub1lem2  14080  ismre  14520  mrcflem  14536  mrcval  14540  ismri  14561  isacs  14581  isacs1i  14587  catlid  14613  catrid  14614  ismon  14664  isnat  14849  eldmcoa  14925  coaval  14928  lubeldm  15143  glbeldm  15156  ismhm  15458  issubm  15466  issubmd  15468  mhmeql  15483  mrcmndind  15485  gsumress  15498  gsumval2  15504  grplinv  15575  issubg  15672  cycsubg  15700  isnsg  15701  ghmeql  15760  isgim  15781  isga  15800  elcntz  15831  elcntzsn  15834  symgfix2  15912  pmtrval  15948  pmtrrn  15954  symgsssg  15964  symgfisg  15965  psgnunilem5  15991  odid  16032  odlem2  16033  gexid  16071  gexlem2  16072  gexdvds  16074  isslw  16098  pgpssslw  16104  pj1id  16187  efgsfo  16227  oddvdssubg  16328  pgpfac1lem5  16568  ablfaclem2  16575  isirred  16779  issubrg  16843  isabv  16882  islss  16993  islmhm  17085  lmhmeql  17113  islmim  17120  islbs  17134  gsumbagdiaglem  17422  psrmulcllem  17435  psrlidm  17451  psrlidmOLD  17452  psrridm  17453  psrridmOLD  17454  psrass1  17455  psrcom  17458  mplsubglem  17487  mpllsslem  17488  mplsubglemOLD  17489  mpllsslemOLD  17490  mplmonmul  17520  evlsval2  17581  coe1mul2  17698  zrhcofipsgn  17998  psgndiflemB  18005  elocv  18068  isobs  18120  dsmmelbas  18139  frlmelbas  18157  frlmelbasOLD  18158  frlmssuvc2  18195  frlmssuvc2OLD  18197  islinds  18213  symgmatr01lem  18434  istopon  18505  fctop  18583  cctop  18585  ppttop  18586  pptbas  18587  epttop  18588  iscld  18606  clscld  18626  isnei  18682  neips  18692  neiptopnei  18711  iscn  18814  iscnp  18816  ordthauslem  18962  cmpsublem  18977  concompcon  19011  2ndc1stc  19030  2ndcdisj  19035  elkgen  19084  xkoopn  19137  xkoccn  19167  txdis1cn  19183  pthaus  19186  txkgen  19200  xkohaus  19201  xkococnlem  19207  xkococn  19208  xkoinjcn  19235  txcon  19237  elqtop  19245  nrmr0reg  19297  elmptrab  19375  fbssfi  19385  opnfbas  19390  elfg  19419  cfinfil  19441  csdfil  19442  supfil  19443  filssufilg  19459  uffix  19469  fixufil  19470  uffixfr  19471  uffixsn  19473  ufinffr  19477  ufilen  19478  elflim2  19512  supnfcls  19568  fclscf  19573  flimfnfcls  19576  alexsubALTlem2  19595  alexsubALTlem4  19597  alexsubALT  19598  ptcmplem2  19600  tmdgsum2  19642  symgtgp  19647  ghmcnp  19660  elutop  19783  isucn  19828  iscfilu  19838  ispsmet  19855  ismet  19873  isxmet  19874  elblps  19937  elbl  19938  restmetu  20137  icccmp  20377  elcncf  20440  ishtpy  20519  isphtpy  20528  om1elbas  20579  iscfil  20751  iscau  20762  iscmet  20770  lmle  20787  rrxfsupp  20876  minveclem3  20891  minveclem4  20894  ovolshftlem1  20967  ovolscalem1  20971  ovolicc2lem3  20977  iundisj  21004  dyadmax  21053  dyadmbllem  21054  opnmbllem  21056  vitalilem2  21064  vitalilem3  21065  elcpn  21383  ig1pval3  21621  coelem  21669  quotlem  21741  elqaalem1  21760  elqaalem3  21762  aannenlem1  21769  aannenlem2  21770  aalioulem2  21774  radcnv0  21856  dmarea  22326  jensen  22357  ftalem4  22388  ftalem5  22389  efnnfsumcl  22415  efchtdvds  22472  sqff1o  22495  dvdsdivcl  22496  fsumdvdsdiaglem  22498  dvdsppwf1o  22501  dvdsflf1o  22502  dvdsflsumcom  22503  musum  22506  muinv  22508  logfac2  22531  dchrelbas  22550  dchrfi  22569  lgsfle1  22619  lgsle1  22625  lgsdirprm  22643  lgsne0  22647  lgsquadlem1  22668  lgsquadlem2  22669  dchrvmasumlem1  22719  logsqvma  22766  pntleml  22835  tgellng  22961  mircgr  23029  mirbtwn  23030  ttgelitv  23080  ebtwntg  23179  umgrale  23206  umgra1  23211  uslgra1  23242  usgra1  23243  usgraedg2  23245  usgraedgrnv  23247  usgrarnedg  23254  usgraedg4  23256  usgraexmpl  23270  usgrares1  23274  nbgrael  23288  nbgraeledg  23292  nbgraf1olem3  23303  cusgrarn  23318  nbcusgra  23322  cusgrares  23331  uvtxel  23348  uvtxnbgra  23352  cusgrauvtxb  23355  eupath2  23552  umgrabi  23555  konigsberg  23559  grpoidinv2  23656  grpoinv  23665  isssp  24073  islno  24104  isblo  24133  ishmo  24162  ubthlem1  24222  ubthlem2  24223  htthlem  24270  ocel  24635  shsval2i  24741  ococin  24762  chsupsn  24767  eleigvec  25312  cnlnadjlem5  25426  shatomistici  25716  hatomistici  25717  nnindf  26040  ordtconlem1  26306  indf1ofs  26434  sigagenval  26535  ddemeas  26604  ismbfm  26619  imambfm  26629  dya2iocuni  26650  oms0  26662  issibf  26671  sitgfval  26679  oddpwdc  26689  eulerpartlemgh  26713  eulerpartlemgs2  26715  dstfrvel  26808  ballotlemfc0  26827  ballotlemfcc  26828  ballotlemiex  26836  ballotlemfrcn0  26864  ballotlemirc  26866  ballotlem7  26870  conpcon  27076  iscvm  27100  cvmsi  27106  cvmsval  27107  cvmliftmolem2  27123  cvmliftiota  27142  snmlval  27172  elgiso  27266  sltval2  27748  sltres  27756  nodenselem7  27779  nofulllem5  27798  lineelsb2  28130  linerflx1  28131  rankeq1o  28160  fin2solem  28368  fin2so  28369  opnmbllem0  28380  mblfinlem2  28382  itg2gt0cn  28400  finminlem  28466  fneint  28502  fnessref  28518  locfincmp  28529  topmeet  28538  topjoin  28539  neifg  28545  indexa  28580  nninfnub  28600  istotbnd  28621  sstotbnd2  28626  isbnd  28632  isrngohom  28724  isrngoiso  28737  isidl  28767  ispridl  28787  ismaxidl  28793  prnc  28820  isfldidl  28821  isnacs  28993  elmzpcl  29015  mzpindd  29035  rencldnfilem  29112  irrapxlem6  29121  pellexlem3  29125  pellexlem5  29127  elpell1qr  29141  elpell14qr  29143  elpell1234qr  29145  pellfundre  29175  pellfundge  29176  pellfundlb  29178  pellfundglb  29179  rmspecnonsq  29201  jm2.22  29297  jm2.23  29298  rpnnen3lem  29333  fnwe2lem2  29357  fnwe2lem3  29358  elmnc  29446  dgraalem  29455  dgraaub  29458  mpaalem  29462  rgspnmin  29481  issdrg  29507  phisum  29520  stoweidlem14  29762  stoweidlem15  29763  stoweidlem16  29764  stoweidlem31  29779  stoweidlem36  29784  stoweidlem46  29794  stoweidlem48  29796  elss2pr  30181  wwlktovf  30204  wwlktovf1  30205  wwlktovfo  30206  iswwlk  30270  iswwlkn  30271  wlknwwlknsur  30297  wlkiswwlksur  30304  wwlkextinj  30315  wwlkextsur  30316  wlknwwlknvbij  30325  el2wlkonot  30341  el2spthonot  30342  el2spthonot0  30343  el2wlksoton  30350  el2spthsoton  30351  el2wlksotot  30354  isclwwlk  30384  isclwwlkn  30385  clwwlkprop  30386  clwwlknprop  30388  clwwlkvbij  30416  Lemma2  30446  eleclclwwlkn  30460  clwlkfclwwlk1hashn  30467  clwlkf1clwwlklem1  30472  clwlkf1clwwlklem2  30473  rusgranumwlklem0  30519  rusgranumwlklem1  30520  rusgranumwlklem3  30522  rusgranumwlks  30527  2spotdisj  30607  usg2spot2nb  30611  usgreg2spot  30613  numclwwlkun  30625  numclwwlkovfel2  30629  numclwwlkovgel  30634  numclwlk1lem2foa  30637  numclwwlk2lem1  30648  numclwlk2lem2f  30649  numclwlk2lem2f1o  30651  coe1fsupp  30769  dmatelnd  30798  dmatsubcl  30800  dmatmulcl  30802  scmatsubcl  30807  scmatmulcl  30809  pmatcollpw2lem  30820  lcoval  30835  secval  30971  cscval  30972  cotval  30973  islshp  32464  lssats  32497  islfl  32545  isat  32771  atlatmstc  32804  islln  32990  islpln  33014  islvol  33057  linepsubN  33236  elpmap  33242  pmapsub  33252  elpadd  33283  paddvaln0N  33285  islhp  33480  isldil  33594  isltrn  33603  isdilN  33638  istrnN  33641  diaval  34517  diaelval  34518  diaeldm  34521  diaelrnN  34530  cdlemm10N  34603  docaclN  34609  dibglbN  34651  dicval  34661  dicfnN  34668  dicvalrelN  34670  dihglblem2aN  34778  dihglblem2N  34779  dihglblem3N  34780  dih1dimatlem  34814  dihglb2  34827  dochvalr  34842  doch2val2  34849  dochocss  34851  islpolN  34968  mapd0  35150
  Copyright terms: Public domain W3C validator