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

Theorem elrab 3257
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 2619 . 2  |-  F/_ x A
2 nfcv 2619 . 2  |-  F/_ x B
3 nfv 1708 . 2  |-  F/ x ps
4 elrab.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
51, 2, 3, 4elrabf 3255 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 1395    e. wcel 1819   {crab 2811
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111
This theorem is referenced by:  elrab3  3258  elrab2  3259  ralrab  3261  rexrab  3263  rabsnt  4109  unimax  4287  ssintub  4306  intminss  4315  reusv6OLD  4667  rabxfrd  4677  ssimaex  5938  weniso  6251  canth  6255  sorpsscmpl  6590  onnminsb  6638  dfom2  6701  ssnlim  6717  elsuppfn  6925  ressuppssdif  6939  oeeulem  7268  nnawordex  7304  elpmg  7453  fineqvlem  7753  mapfienlem2  7883  supub  7936  suplub  7937  ordtypelem6  7966  ordtypelem7  7967  hartogslem1  7985  hartogs  7987  wemapsolem  7993  card2on  7998  elharval  8007  wdom2d  8024  cantnfs  8102  oemapvali  8120  cantnfsOLD  8132  rankuni2b  8288  scottex  8320  tskwe  8348  cardid2  8351  iscard2  8374  harval2  8395  cardmin2  8396  acni3  8445  alephsuc2  8478  kmlem1  8547  cofsmo  8666  coftr  8670  fin23lem11  8714  enfin2i  8718  fin1a2lem9  8805  fin1a2lem11  8807  axcc4  8836  axdc3lem2  8848  zorn2lem7  8899  ondomon  8955  alephval2  8964  grutsk  9217  pinq  9322  infm3  10522  infmrcl  10542  nnind  10574  peano2uz2  10971  peano5uzi  10972  dfuzi  10974  uzind  10975  uzind3  10977  uzind3OLD  10979  eluz1  11110  uzind4  11164  nnwos  11174  eqreznegel  11192  zsupss  11196  zmin  11203  elixx1  11563  elioo2  11595  elfz1  11702  flval3  11953  serge0  12163  expge0  12204  expge1  12205  hashbclem  12504  pr2pwpr  12523  elss2pr  12530  wrdmap  12579  wwlktovfo  12907  shftf  12923  rlimrege0  13413  incexc2  13661  divalglem4  14065  divalgmod  14075  bitsval  14085  bezout  14191  1nprm  14233  1idssfct  14234  isprm2  14236  phicl2  14309  hashdvds  14316  odzval  14329  odzcllem  14330  odzdvds  14333  pcpremul  14378  prmreclem1  14445  prmreclem2  14446  prmreclem3  14447  prmreclem5  14449  ramub  14542  rami  14544  ramub1lem1  14555  ramub1lem2  14556  ismre  15006  mrcflem  15022  mrcval  15026  ismri  15047  isacs  15067  isacs1i  15073  catlid  15099  catrid  15100  ismon  15148  isnat  15362  eldmcoa  15470  coaval  15473  fncnvimaeqv  15515  lubeldm  15737  glbeldm  15750  gsumress  16029  gsumval2  16033  ismhm  16094  issubm  16104  issubmd  16106  mhmeql  16121  mrcmndind  16123  grplinv  16222  issubg  16327  cycsubg  16355  isnsg  16356  ghmeql  16415  isgim  16436  isga  16455  elcntz  16486  elcntzsn  16489  symgfix2  16567  pmtrval  16602  pmtrrn  16608  symgsssg  16618  symgfisg  16619  psgnunilem5  16645  odid  16688  odlem2  16689  gexid  16727  gexlem2  16728  gexdvds  16730  isslw  16754  pgpssslw  16760  pj1id  16843  efgsfo  16883  oddvdssubg  16987  dprdwd  17170  pgpfac1lem5  17256  ablfaclem2  17263  isirred  17474  isrim0  17498  issubrg  17555  isabv  17594  islss  17707  islmhm  17799  lmhmeql  17827  islmim  17834  islbs  17848  gsumbagdiaglem  18153  psrmulcllem  18166  psrlidm  18182  psrlidmOLD  18183  psrridm  18184  psrridmOLD  18185  psrass1  18186  psrcom  18190  mplsubglem  18219  mpllsslem  18220  mplsubglemOLD  18221  mpllsslemOLD  18222  mplmonmul  18252  evlsval2  18315  coe1fsupp  18380  coe1ae0  18383  coe1mul2  18436  zrhcofipsgn  18755  psgndiflemB  18762  elocv  18825  isobs  18877  dsmmelbas  18896  frlmelbas  18914  frlmelbasOLD  18915  frlmssuvc2  18952  frlmssuvc2OLD  18954  islinds  18970  dmatel  19121  dmatmulcl  19128  scmatel  19133  scmateALT  19140  symgmatr01lem  19281  pmatcoe1fsupp  19328  cpmatel  19338  chpscmat  19469  istopon  19552  fctop  19631  cctop  19633  ppttop  19634  pptbas  19635  epttop  19636  iscld  19654  clscld  19674  isnei  19730  neips  19740  neiptopnei  19759  iscn  19862  iscnp  19864  ordthauslem  20010  cmpsublem  20025  concompcon  20058  2ndc1stc  20077  2ndcdisj  20082  locfincmp  20152  elkgen  20162  xkoopn  20215  xkoccn  20245  txdis1cn  20261  pthaus  20264  txkgen  20278  xkohaus  20279  xkococnlem  20285  xkococn  20286  xkoinjcn  20313  txcon  20315  elqtop  20323  nrmr0reg  20375  elmptrab  20453  fbssfi  20463  opnfbas  20468  elfg  20497  cfinfil  20519  csdfil  20520  supfil  20521  filssufilg  20537  uffix  20547  fixufil  20548  uffixfr  20549  uffixsn  20551  ufinffr  20555  ufilen  20556  elflim2  20590  supnfcls  20646  fclscf  20651  flimfnfcls  20654  alexsubALTlem2  20673  alexsubALTlem4  20675  alexsubALT  20676  ptcmplem2  20678  tmdgsum2  20720  symgtgp  20725  ghmcnp  20738  elutop  20861  isucn  20906  iscfilu  20916  ispsmet  20933  ismet  20951  isxmet  20952  elblps  21015  elbl  21016  restmetu  21215  icccmp  21455  elcncf  21518  ishtpy  21597  isphtpy  21606  om1elbas  21657  iscfil  21829  iscau  21840  iscmet  21848  lmle  21865  rrxfsupp  21954  minveclem3  21969  minveclem4  21972  ovolshftlem1  22045  ovolscalem1  22049  ovolicc2lem3  22055  iundisj  22083  dyadmax  22132  dyadmbllem  22133  opnmbllem  22135  vitalilem2  22143  vitalilem3  22144  elcpn  22462  ig1pval3  22700  coelem  22748  quotlem  22821  elqaalem1  22840  elqaalem3  22842  aannenlem1  22849  aannenlem2  22850  aalioulem2  22854  radcnv0  22936  dmarea  23412  jensen  23443  ftalem4  23474  ftalem5  23475  efnnfsumcl  23501  efchtdvds  23558  sqff1o  23581  dvdsdivcl  23582  fsumdvdsdiaglem  23584  dvdsppwf1o  23587  dvdsflf1o  23588  dvdsflsumcom  23589  musum  23592  muinv  23594  logfac2  23617  dchrelbas  23636  dchrfi  23655  lgsfle1  23705  lgsle1  23711  lgsdirprm  23729  lgsne0  23733  lgsquadlem1  23754  lgsquadlem2  23755  dchrvmasumlem1  23805  logsqvma  23852  pntleml  23921  tgellng  24065  mircgr  24163  mirbtwn  24164  ttgelitv  24312  umgrale  24447  umgra1  24452  edg  24479  uslgra1  24498  usgra1  24499  usgraedg2  24501  usgraedgrnv  24503  usgrarnedg  24510  usgraedg4  24513  usgraexmpl  24527  usgrares1  24536  nbgrael  24552  nbgraeledg  24556  nbgraf1olem3  24569  cusgrarn  24585  nbcusgra  24589  cusgrares  24598  uvtxel  24615  uvtxnbgra  24619  cusgrauvtxb  24622  iswwlk  24809  iswwlkn  24810  wlknwwlknsur  24838  wlkiswwlksur  24845  wwlkextsur  24857  wlknwwlknvbij  24866  isclwwlk  24894  isclwwlkn  24895  clwwlkprop  24896  clwwlknprop  24898  clwwlkvbij  24927  clwwlknscsh  24945  eleclclwwlkn  24959  el2wlkonot  24995  el2spthonot  24996  el2spthonot0  24997  el2wlksoton  25004  el2spthsoton  25005  el2wlksotot  25008  rusgranumwlklem0  25074  rusgranumwlklem1  25075  rusgranumwlklem3  25077  rusgranumwlks  25082  eupath2  25106  umgrabi  25109  konigsberg  25113  2spotdisj  25187  usg2spot2nb  25191  usgreg2spot  25193  numclwwlkun  25205  numclwwlkovfel2  25209  numclwwlkovgel  25214  numclwlk1lem2foa  25217  numclwwlk2lem1  25228  numclwlk2lem2f  25229  numclwlk2lem2f1o  25231  grpoidinv2  25346  grpoinv  25355  isssp  25763  islno  25794  isblo  25823  ishmo  25852  ubthlem1  25912  ubthlem2  25913  htthlem  25960  ocel  26325  shsval2i  26431  ococin  26452  chsupsn  26457  eleigvec  27002  cnlnadjlem5  27116  shatomistici  27406  hatomistici  27407  nnindf  27762  ordtconlem1  28059  indf1ofs  28192  sigagenval  28301  ddemeas  28369  ismbfm  28384  imambfm  28394  dya2iocuni  28415  oms0  28429  omssubadd  28432  elcarsg  28437  issibf  28450  sitgfval  28458  oddpwdc  28468  eulerpartlemgh  28492  eulerpartlemgs2  28494  dstfrvel  28587  ballotlemfc0  28606  ballotlemfcc  28607  ballotlemiex  28615  ballotlemfrcn0  28643  ballotlemirc  28645  ballotlem7  28649  conpcon  28855  iscvm  28879  cvmsi  28885  cvmsval  28886  cvmliftmolem2  28902  cvmliftiota  28921  snmlval  28951  elmpst  29071  elgiso  29211  sltval2  29590  sltres  29598  nodenselem7  29621  nofulllem5  29640  lineelsb2  29960  linerflx1  29961  rankeq1o  29990  fin2solem  30201  fin2so  30202  opnmbllem0  30212  mblfinlem2  30214  itg2gt0cn  30232  finminlem  30298  fneint  30328  fnessref  30337  topmeet  30344  topjoin  30345  neifg  30351  indexa  30386  nninfnub  30406  istotbnd  30427  sstotbnd2  30432  isbnd  30438  isrngohom  30530  isrngoiso  30543  isidl  30573  ispridl  30593  ismaxidl  30599  prnc  30626  isfldidl  30627  isnacs  30798  elmzpcl  30820  mzpindd  30840  rencldnfilem  30916  irrapxlem6  30925  pellexlem3  30929  pellexlem5  30931  elpell1qr  30945  elpell14qr  30947  elpell1234qr  30949  pellfundre  30979  pellfundge  30980  pellfundlb  30982  pellfundglb  30983  rmspecnonsq  31005  jm2.22  31099  jm2.23  31100  rpnnen3lem  31135  fnwe2lem2  31159  fnwe2lem3  31160  elmnc  31247  dgraalem  31256  dgraaub  31259  mpaalem  31263  rgspnmin  31282  issdrg  31308  phisum  31321  lcmledvds  31367  lcmgcdlem  31374  nzss  31384  iccshift  31719  iooshift  31723  limcperiod  31795  sumnnodd  31797  ioodvbdlimc1lem1  31889  dvnprodlem1  31904  dvnprodlem3  31906  itgperiod  31941  stoweidlem14  31957  stoweidlem15  31958  stoweidlem16  31959  stoweidlem31  31974  stoweidlem36  31979  stoweidlem46  31989  stoweidlem48  31991  fourierdlem2  32052  fourierdlem3  32053  fourierdlem20  32070  fourierdlem25  32075  fourierdlem37  32087  fourierdlem42  32092  fourierdlem48  32098  fourierdlem51  32101  fourierdlem63  32113  fourierdlem64  32114  fourierdlem65  32115  fourierdlem79  32129  fourierdlem81  32131  elaa2lem  32177  etransclem24  32202  etransclem26  32204  etransclem28  32206  etransclem35  32213  etransclem48  32226  ismgmhm  32691  issubmgm  32697  rabsubmgmd  32699  mgmhmeql  32711  assintop  32753  isassintop  32754  assintopcllaw  32756  isrnghm  32800  isrngisom  32804  0even  32839  2even  32841  2zrngamgm  32847  dmatALTbasel  33105  lcoval  33115  secval  33243  cscval  33244  cotval  33245  islshp  34805  lssats  34838  islfl  34886  isat  35112  atlatmstc  35145  islln  35331  islpln  35355  islvol  35398  linepsubN  35577  elpmap  35583  pmapsub  35593  elpadd  35624  paddvaln0N  35626  islhp  35821  isldil  35935  isltrn  35944  isdilN  35980  istrnN  35983  diaval  36860  diaelval  36861  diaeldm  36864  diaelrnN  36873  cdlemm10N  36946  docaclN  36952  dibglbN  36994  dicval  37004  dicfnN  37011  dicvalrelN  37013  dihglblem2aN  37121  dihglblem2N  37122  dihglblem3N  37123  dih1dimatlem  37157  dihglb2  37170  dochvalr  37185  doch2val2  37192  dochocss  37194  islpolN  37311  mapd0  37493
  Copyright terms: Public domain W3C validator