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

Theorem elrab 3206
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 2564 . 2  |-  F/_ x A
2 nfcv 2564 . 2  |-  F/_ x B
3 nfv 1728 . 2  |-  F/ x ps
4 elrab.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
51, 2, 3, 4elrabf 3204 1  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1405    e. wcel 1842   {crab 2757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2762  df-v 3060
This theorem is referenced by:  elrab3  3207  elrab2  3208  ralrab  3210  rexrab  3212  rabsnt  4048  unimax  4225  ssintub  4244  intminss  4253  rabxfrd  4611  ssimaex  5870  weniso  6189  canth  6193  sorpsscmpl  6529  onnminsb  6577  dfom2  6640  ssnlim  6656  elsuppfn  6864  ressuppssdif  6878  oeeulem  7207  nnawordex  7243  elpmg  7392  fineqvlem  7689  mapfienlem2  7819  supub  7872  suplub  7873  ordtypelem6  7902  ordtypelem7  7903  hartogslem1  7921  hartogs  7923  wemapsolem  7929  card2on  7934  elharval  7943  wdom2d  7960  cantnfs  8037  oemapvali  8055  cantnfsOLD  8067  rankuni2b  8223  scottex  8255  tskwe  8283  cardid2  8286  iscard2  8309  harval2  8330  cardmin2  8331  acni3  8380  alephsuc2  8413  kmlem1  8482  cofsmo  8601  coftr  8605  fin23lem11  8649  enfin2i  8653  fin1a2lem9  8740  fin1a2lem11  8742  axcc4  8771  axdc3lem2  8783  zorn2lem7  8834  ondomon  8890  alephval2  8899  grutsk  9150  pinq  9255  infm3  10462  infmrcl  10482  nnind  10514  peano2uz2  10911  peano5uzi  10912  dfuzi  10914  uzind  10915  uzind3  10917  eluz1  11049  uzind4  11103  nnwos  11112  eqreznegel  11130  zsupss  11134  zmin  11141  elixx1  11509  elioo2  11541  elfz1  11648  flval3  11901  serge0  12115  expge0  12156  expge1  12157  hashbclem  12457  pr2pwpr  12476  elss2pr  12483  wrdmap  12532  wwlktovfo  12859  shftf  12968  rlimrege0  13458  incexc2  13708  divalglem4  14155  divalgmod  14165  bitsval  14175  bezout  14281  1nprm  14323  1idssfct  14324  isprm2  14326  phicl2  14399  hashdvds  14406  odzval  14419  odzcllem  14420  odzdvds  14423  pcpremul  14468  prmreclem1  14535  prmreclem2  14536  prmreclem3  14537  prmreclem5  14539  ramub  14632  rami  14634  ramub1lem1  14645  ramub1lem2  14646  ismre  15096  mrcflem  15112  mrcval  15116  ismri  15137  isacs  15157  isacs1i  15163  catlid  15189  catrid  15190  ismon  15238  isnat  15452  eldmcoa  15560  coaval  15563  fncnvimaeqv  15605  lubeldm  15827  glbeldm  15840  gsumress  16119  gsumval2  16123  ismhm  16184  issubm  16194  issubmd  16196  mhmeql  16211  mrcmndind  16213  grplinv  16312  issubg  16417  cycsubg  16445  isnsg  16446  ghmeql  16505  isgim  16526  isga  16545  elcntz  16576  elcntzsn  16579  symgfix2  16657  pmtrval  16692  pmtrrn  16698  symgsssg  16708  symgfisg  16709  psgnunilem5  16735  odid  16778  odlem2  16779  gexid  16817  gexlem2  16818  gexdvds  16820  isslw  16844  pgpssslw  16850  pj1id  16933  efgsfo  16973  oddvdssubg  17077  dprdwd  17256  pgpfac1lem5  17342  ablfaclem2  17349  isirred  17560  isrim0  17584  issubrg  17641  isabv  17680  islss  17793  islmhm  17885  lmhmeql  17913  islmim  17920  islbs  17934  gsumbagdiaglem  18239  psrmulcllem  18252  psrlidm  18268  psrlidmOLD  18269  psrridm  18270  psrridmOLD  18271  psrass1  18272  psrcom  18276  mplsubglem  18305  mpllsslem  18306  mplsubglemOLD  18307  mpllsslemOLD  18308  mplmonmul  18338  evlsval2  18401  coe1fsupp  18466  coe1ae0  18469  coe1mul2  18522  zrhcofipsgn  18819  psgndiflemB  18826  elocv  18889  isobs  18941  dsmmelbas  18960  frlmelbas  18978  frlmssuvc2  19014  islinds  19028  dmatel  19179  dmatmulcl  19186  scmatel  19191  scmateALT  19198  symgmatr01lem  19339  pmatcoe1fsupp  19386  cpmatel  19396  chpscmat  19527  istopon  19610  fctop  19689  cctop  19691  ppttop  19692  pptbas  19693  epttop  19694  iscld  19712  clscld  19732  isnei  19789  neips  19799  neiptopnei  19818  iscn  19921  iscnp  19923  ordthauslem  20069  cmpsublem  20084  concompcon  20117  2ndc1stc  20136  2ndcdisj  20141  locfincmp  20211  elkgen  20221  xkoopn  20274  xkoccn  20304  txdis1cn  20320  pthaus  20323  txkgen  20337  xkohaus  20338  xkococnlem  20344  xkococn  20345  xkoinjcn  20372  txcon  20374  elqtop  20382  nrmr0reg  20434  elmptrab  20512  fbssfi  20522  opnfbas  20527  elfg  20556  cfinfil  20578  csdfil  20579  supfil  20580  filssufilg  20596  uffix  20606  fixufil  20607  uffixfr  20608  uffixsn  20610  ufinffr  20614  ufilen  20615  elflim2  20649  supnfcls  20705  fclscf  20710  flimfnfcls  20713  alexsubALTlem2  20732  alexsubALTlem4  20734  alexsubALT  20735  ptcmplem2  20737  tmdgsum2  20779  symgtgp  20784  ghmcnp  20797  elutop  20920  isucn  20965  iscfilu  20975  ispsmet  20992  ismet  21010  isxmet  21011  elblps  21074  elbl  21075  restmetu  21274  icccmp  21514  elcncf  21577  ishtpy  21656  isphtpy  21665  om1elbas  21716  iscfil  21888  iscau  21899  iscmet  21907  lmle  21924  rrxfsupp  22013  minveclem3  22028  minveclem4  22031  ovolshftlem1  22104  ovolscalem1  22108  ovolicc2lem3  22114  iundisj  22142  dyadmax  22191  dyadmbllem  22192  opnmbllem  22194  vitalilem2  22202  vitalilem3  22203  elcpn  22521  ig1pval3  22759  coelem  22807  quotlem  22880  elqaalem1  22899  elqaalem3  22901  aannenlem1  22908  aannenlem2  22909  aalioulem2  22913  radcnv0  22995  dmarea  23505  jensen  23536  ftalem4  23622  ftalem5  23623  efnnfsumcl  23649  efchtdvds  23706  sqff1o  23729  dvdsdivcl  23730  fsumdvdsdiaglem  23732  dvdsppwf1o  23735  dvdsflf1o  23736  dvdsflsumcom  23737  musum  23740  muinv  23742  logfac2  23765  dchrelbas  23784  dchrfi  23803  lgsfle1  23853  lgsle1  23859  lgsdirprm  23877  lgsne0  23881  lgsquadlem1  23902  lgsquadlem2  23903  dchrvmasumlem1  23953  logsqvma  24000  pntleml  24069  tgellng  24215  mircgr  24315  mirbtwn  24316  ttgelitv  24484  umgrale  24619  umgra1  24624  edg  24651  uslgra1  24670  usgra1  24671  usgraedg2  24673  usgraedgrnv  24675  usgrarnedg  24682  usgraedg4  24685  usgraexmpl  24699  usgrares1  24708  nbgrael  24724  nbgraeledg  24728  nbgraf1olem3  24741  cusgrarn  24757  nbcusgra  24761  cusgrares  24770  uvtxel  24787  uvtxnbgra  24791  cusgrauvtxb  24794  iswwlk  24981  iswwlkn  24982  wlknwwlknsur  25010  wlkiswwlksur  25017  wwlkextsur  25029  wlknwwlknvbij  25038  isclwwlk  25066  isclwwlkn  25067  clwwlkprop  25068  clwwlknprop  25070  clwwlkvbij  25099  clwwlknscsh  25117  eleclclwwlkn  25131  el2wlkonot  25167  el2spthonot  25168  el2spthonot0  25169  el2wlksoton  25176  el2spthsoton  25177  el2wlksotot  25180  rusgranumwlklem0  25246  rusgranumwlklem1  25247  rusgranumwlklem3  25249  rusgranumwlks  25254  eupath2  25278  umgrabi  25281  konigsberg  25285  2spotdisj  25359  usg2spot2nb  25363  usgreg2spot  25365  numclwwlkun  25377  numclwwlkovfel2  25381  numclwwlkovgel  25386  numclwlk1lem2foa  25389  numclwwlk2lem1  25400  numclwlk2lem2f  25401  numclwlk2lem2f1o  25403  grpoidinv2  25514  grpoinv  25523  isssp  25931  islno  25962  isblo  25991  ishmo  26020  ubthlem1  26080  ubthlem2  26081  htthlem  26128  ocel  26493  shsval2i  26599  ococin  26620  chsupsn  26625  eleigvec  27169  cnlnadjlem5  27283  shatomistici  27573  hatomistici  27574  nnindf  27941  ordtconlem1  28239  indf1ofs  28353  sigagenval  28468  ldsysgenld  28488  ldgenpisyslem1  28491  ldgenpisyslem2  28492  ldgenpisys  28494  ddemeas  28565  ismbfm  28580  imambfm  28590  dya2iocuni  28611  oms0  28625  omssubadd  28628  elcarsg  28633  issibf  28661  sitgfval  28669  oddpwdc  28679  eulerpartlemgh  28703  eulerpartlemgs2  28705  dstfrvel  28798  ballotlemfc0  28817  ballotlemfcc  28818  ballotlemiex  28826  ballotlemfrcn0  28854  ballotlemirc  28856  ballotlem7  28860  conpcon  29413  iscvm  29437  cvmsi  29443  cvmsval  29444  cvmliftmolem2  29460  cvmliftiota  29479  snmlval  29509  elmpst  29629  elgiso  29769  sltval2  30089  sltres  30097  nodenselem7  30120  nofulllem5  30139  lineelsb2  30459  linerflx1  30460  fwddifval  30488  fwddifnval  30489  rankeq1o  30497  finminlem  30534  fneint  30564  fnessref  30573  topmeet  30580  topjoin  30581  neifg  30587  relowlssretop  31267  fin2solem  31392  fin2so  31393  opnmbllem0  31403  mblfinlem2  31405  itg2gt0cn  31424  indexa  31487  nninfnub  31507  istotbnd  31528  sstotbnd2  31533  isbnd  31539  isrngohom  31631  isrngoiso  31644  isidl  31674  ispridl  31694  ismaxidl  31700  prnc  31727  isfldidl  31728  islshp  31978  lssats  32011  islfl  32059  isat  32285  atlatmstc  32318  islln  32504  islpln  32528  islvol  32571  linepsubN  32750  elpmap  32756  pmapsub  32766  elpadd  32797  paddvaln0N  32799  islhp  32994  isldil  33108  isltrn  33117  isdilN  33153  istrnN  33156  diaval  34033  diaelval  34034  diaeldm  34037  diaelrnN  34046  cdlemm10N  34119  docaclN  34125  dibglbN  34167  dicval  34177  dicfnN  34184  dicvalrelN  34186  dihglblem2aN  34294  dihglblem2N  34295  dihglblem3N  34296  dih1dimatlem  34330  dihglb2  34343  dochvalr  34358  doch2val2  34365  dochocss  34367  islpolN  34484  mapd0  34666  isnacs  34979  elmzpcl  35001  mzpindd  35021  rencldnfilem  35096  irrapxlem6  35105  pellexlem3  35109  pellexlem5  35111  elpell1qr  35125  elpell14qr  35127  elpell1234qr  35129  pellfundre  35159  pellfundge  35160  pellfundlb  35162  pellfundglb  35163  rmspecnonsq  35185  jm2.22  35280  jm2.23  35281  rpnnen3lem  35316  fnwe2lem2  35340  fnwe2lem3  35341  elmnc  35430  dgraalem  35439  dgraaub  35442  mpaalem  35446  rgspnmin  35465  issdrg  35491  phisum  35504  lcmledvds  36034  lcmgcdlem  36041  nzss  36051  iccshift  36908  iooshift  36912  limcperiod  36984  sumnnodd  36986  ioodvbdlimc1lem1  37078  dvnprodlem1  37093  dvnprodlem3  37095  itgperiod  37130  stoweidlem14  37146  stoweidlem15  37147  stoweidlem16  37148  stoweidlem31  37163  stoweidlem36  37168  stoweidlem46  37178  stoweidlem48  37180  fourierdlem2  37241  fourierdlem3  37242  fourierdlem20  37259  fourierdlem25  37264  fourierdlem37  37276  fourierdlem42  37281  fourierdlem48  37287  fourierdlem51  37290  fourierdlem63  37302  fourierdlem64  37303  fourierdlem65  37304  fourierdlem79  37318  fourierdlem81  37320  elaa2lem  37366  etransclem24  37391  etransclem26  37393  etransclem28  37395  etransclem35  37402  etransclem48  37415  iccpart  37663  iseven  37690  isodd  37691  dfodd2  37699  dfeven5  37729  dfodd7  37730  ismgmhm  38080  issubmgm  38086  rabsubmgmd  38088  mgmhmeql  38100  assintop  38142  isassintop  38143  assintopcllaw  38145  isrnghm  38189  isrngisom  38193  0even  38228  2even  38230  2zrngamgm  38236  dmatALTbasel  38494  lcoval  38504  elbigo  38662  secval  38767  cscval  38768  cotval  38769
  Copyright terms: Public domain W3C validator