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

Theorem elrab 3184
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 2612 . 2  |-  F/_ x A
2 nfcv 2612 . 2  |-  F/_ x B
3 nfv 1769 . 2  |-  F/ x ps
4 elrab.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
51, 2, 3, 4elrabf 3182 1  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 376    = wceq 1452    e. wcel 1904   {crab 2760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rab 2765  df-v 3033
This theorem is referenced by:  elrab3  3185  elrab2  3186  ralrab  3188  rexrab  3190  rabsnt  4040  unimax  4225  ssintub  4244  intminss  4252  rabxfrd  4621  ssimaex  5945  weniso  6263  canth  6267  sorpsscmpl  6601  onnminsb  6650  dfom2  6713  ssnlim  6729  elsuppfn  6941  ressuppssdif  6955  oeeulem  7320  nnawordex  7356  elpmg  7505  fineqvlem  7804  mapfienlem2  7937  supub  7991  suplub  7992  ordtypelem6  8056  ordtypelem7  8057  hartogslem1  8075  hartogs  8077  wemapsolem  8083  card2on  8087  elharval  8096  wdom2d  8113  cantnfs  8189  oemapvali  8207  rankuni2b  8342  scottex  8374  tskwe  8402  cardid2  8405  iscard2  8428  harval2  8449  cardmin2  8450  acni3  8496  alephsuc2  8529  kmlem1  8598  cofsmo  8717  coftr  8721  fin23lem11  8765  enfin2i  8769  fin1a2lem9  8856  fin1a2lem11  8858  axcc4  8887  axdc3lem2  8899  zorn2lem7  8950  ondomon  9006  alephval2  9015  grutsk  9265  pinq  9370  negf1o  10070  fiminre  10577  infm3  10590  infmrclOLD  10615  nnind  10649  peano2uz2  11046  peano5uzi  11047  dfuzi  11049  uzind  11050  uzind3  11052  eluz1  11186  uzind4  11240  nnwos  11249  eqreznegel  11272  zsupss  11276  zmin  11283  elixx1  11669  elioo2  11702  elfz1  11815  flval3  12083  serge0  12305  expge0  12346  expge1  12347  hashbclem  12656  pr2pwpr  12677  elss2prb  12684  hash2sspr  12685  elss2prOLD  12686  wrdmap  12749  wwlktovfo  13108  shftf  13219  rlimrege0  13720  incexc2  13973  divalglem4  14454  divalgmod  14466  bitsval  14476  bezout  14589  lcmledvds  14643  lcmgcdlem  14650  lcmsledvdsOLD  14664  lcmfledvds  14684  1nprm  14708  1idssfct  14709  isprm2  14711  phicl2  14795  hashdvds  14802  odzval  14815  odzcllem  14816  odzdvds  14819  odzvalOLD  14821  odzcllemOLD  14822  odzdvdsOLD  14825  pcpremul  14872  prmreclem1  14939  prmreclem2  14940  prmreclem3  14941  prmreclem5  14943  ramub  15049  rami  15051  ramub1lem1  15063  ramub1lem2  15064  prmgaplem3  15102  prmgaplem4  15103  prmgaplem5  15104  prmgaplem6  15105  ismre  15574  mrcflem  15590  mrcval  15594  ismri  15615  isacs  15635  isacs1i  15641  catlid  15667  catrid  15668  ismon  15716  isnat  15930  eldmcoa  16038  coaval  16041  fncnvimaeqv  16083  lubeldm  16305  glbeldm  16318  gsumress  16597  gsumval2  16601  ismhm  16662  issubm  16672  issubmd  16674  mhmeql  16689  mrcmndind  16691  grplinv  16790  issubg  16895  cycsubg  16923  isnsg  16924  ghmeql  16983  isgim  17004  isga  17023  elcntz  17054  elcntzsn  17057  symgfix2  17135  pmtrval  17170  pmtrrn  17176  symgsssg  17186  symgfisg  17187  psgnunilem5  17213  odid  17265  odlem2  17266  odidOLD  17281  odlem2OLD  17282  gexid  17310  gexlem2  17311  gexdvds  17313  gexlem2OLD  17314  isslw  17338  pgpssslw  17344  pj1id  17427  efgsfo  17467  oddvdssubg  17571  dprdwd  17721  pgpfac1lem5  17790  ablfaclem2  17797  isirred  18005  isrim0  18029  issubrg  18086  isabv  18125  islss  18236  islmhm  18328  lmhmeql  18356  islmim  18363  islbs  18377  gsumbagdiaglem  18676  psrmulcllem  18688  psrlidm  18704  psrridm  18705  psrass1  18706  psrcom  18710  mplsubglem  18735  mpllsslem  18736  mplmonmul  18765  evlsval2  18820  coe1fsupp  18884  coe1ae0  18886  coe1mul2  18939  zrhcofipsgn  19238  psgndiflemB  19245  elocv  19308  isobs  19360  dsmmelbas  19379  frlmelbas  19396  frlmssuvc2  19430  islinds  19444  dmatel  19595  dmatmulcl  19602  scmatel  19607  scmateALT  19614  symgmatr01lem  19755  pmatcoe1fsupp  19802  cpmatel  19812  chpscmat  19943  istopon  20017  fctop  20096  cctop  20098  ppttop  20099  pptbas  20100  epttop  20101  iscld  20119  clscld  20139  isnei  20196  neips  20206  neiptopnei  20225  iscn  20328  iscnp  20330  ordthauslem  20476  cmpsublem  20491  concompcon  20524  2ndc1stc  20543  2ndcdisj  20548  locfincmp  20618  elkgen  20628  xkoopn  20681  xkoccn  20711  txdis1cn  20727  pthaus  20730  txkgen  20744  xkohaus  20745  xkococnlem  20751  xkococn  20752  xkoinjcn  20779  txcon  20781  elqtop  20789  nrmr0reg  20841  elmptrab  20919  fbssfi  20930  opnfbas  20935  elfg  20964  cfinfil  20986  csdfil  20987  supfil  20988  filssufilg  21004  uffix  21014  fixufil  21015  uffixfr  21016  uffixsn  21018  ufinffr  21022  ufilen  21023  elflim2  21057  supnfcls  21113  fclscf  21118  flimfnfcls  21121  alexsubALTlem2  21141  alexsubALTlem4  21143  alexsubALT  21144  ptcmplem2  21146  tmdgsum2  21189  symgtgp  21194  ghmcnp  21207  elutop  21326  isucn  21371  iscfilu  21381  ispsmet  21398  ismet  21416  isxmet  21417  elblps  21480  elbl  21481  restmetu  21663  icccmp  21921  elcncf  21999  ishtpy  22081  isphtpy  22090  om1elbas  22141  iscfil  22313  iscau  22324  iscmet  22332  lmle  22349  rrxfsupp  22434  minveclem3  22449  minveclem4  22452  minveclem3OLD  22461  minveclem4OLD  22464  ovolshftlem1  22540  ovolscalem1  22544  ovolicc2lem3  22550  iundisj  22580  dyadmax  22635  dyadmbllem  22636  opnmbllem  22638  vitalilem2  22646  vitalilem3  22647  elcpn  22967  ig1pval3  23205  ig1pval3OLD  23211  coelem  23259  quotlem  23332  elqaalem1  23351  elqaalem3  23353  elqaalem1OLD  23354  elqaalem3OLD  23356  aannenlem1  23363  aannenlem2  23364  aalioulem2  23368  radcnv0  23450  dmarea  23962  jensen  23993  ftalem4  24079  ftalem5  24080  ftalem4OLD  24081  ftalem5OLD  24082  efnnfsumcl  24108  efchtdvds  24165  sqff1o  24188  dvdsdivcl  24189  fsumdvdsdiaglem  24191  dvdsppwf1o  24194  dvdsflf1o  24195  dvdsflsumcom  24196  musum  24199  muinv  24201  logfac2  24224  dchrelbas  24243  dchrfi  24262  lgsfle1  24312  lgsle1  24318  lgsdirprm  24336  lgsne0  24340  lgsquadlem1  24361  lgsquadlem2  24362  dchrvmasumlem1  24412  logsqvma  24459  pntleml  24528  tgellng  24677  mircgr  24781  mirbtwn  24782  iseqlg  24976  ttgelitv  24992  umgrale  25127  umgra1  25132  edg  25159  uslgra1  25178  usgra1  25179  usgraedg2  25181  usgraedgrnv  25183  usgrarnedg  25190  usgraedg4  25193  usgraexmplef  25207  usgrares1  25217  nbgrael  25233  nbgraeledg  25237  nbgraf1olem3  25250  cusgrarn  25266  nbcusgra  25270  cusgrares  25279  uvtxel  25296  uvtxnbgra  25300  cusgrauvtxb  25303  iswwlk  25490  iswwlkn  25491  wlknwwlknsur  25519  wlkiswwlksur  25526  wwlkextsur  25538  wlknwwlknvbij  25547  isclwwlk  25575  isclwwlkn  25576  clwwlkprop  25577  clwwlknprop  25579  clwwlkvbij  25608  clwwlknscsh  25626  eleclclwwlkn  25640  el2wlkonot  25676  el2spthonot  25677  el2spthonot0  25678  el2wlksoton  25685  el2spthsoton  25686  el2wlksotot  25689  rusgranumwlklem0  25755  rusgranumwlklem1  25756  rusgranumwlklem3  25758  rusgranumwlks  25763  eupath2  25787  umgrabi  25790  konigsberg  25794  2spotdisj  25868  usg2spot2nb  25872  usgreg2spot  25874  numclwwlkun  25886  numclwwlkovfel2  25890  numclwwlkovgel  25895  numclwlk1lem2foa  25898  numclwwlk2lem1  25909  numclwlk2lem2f  25910  numclwlk2lem2f1o  25912  grpoidinv2  26027  grpoinv  26036  isssp  26444  islno  26475  isblo  26504  ishmo  26533  ubthlem1  26593  ubthlem2  26594  htthlem  26651  ocel  27015  shsval2i  27121  ococin  27142  chsupsn  27147  eleigvec  27691  cnlnadjlem5  27805  shatomistici  28095  hatomistici  28096  nnindf  28457  ordtconlem1  28804  indf1ofs  28921  sigagenval  29036  ldsysgenld  29056  ldgenpisyslem1  29059  ldgenpisyslem2  29060  ldgenpisys  29062  ddemeas  29132  ismbfm  29147  imambfm  29157  dya2iocuni  29178  oms0  29198  omssubadd  29201  oms0OLD  29202  omssubaddOLD  29205  elcarsg  29210  issibf  29239  sitgfval  29247  oddpwdc  29260  eulerpartlemgh  29284  eulerpartlemgs2  29286  dstfrvel  29379  ballotlemfc0  29398  ballotlemfcc  29399  ballotlemiex  29407  ballotlemfrcn0  29435  ballotlemirc  29437  ballotlem7  29441  ballotlemiexOLD  29445  ballotlemfrcn0OLD  29473  ballotlemircOLD  29475  ballotlem7OLD  29479  conpcon  30030  iscvm  30054  cvmsi  30060  cvmsval  30061  cvmliftmolem2  30077  cvmliftiota  30096  snmlval  30126  elmpst  30246  elgiso  30386  sltval2  30614  sltres  30622  nodenselem7  30647  nofulllem5  30666  lineelsb2  30986  linerflx1  30987  fwddifval  31000  fwddifnval  31001  rankeq1o  31009  finminlem  31045  fneint  31075  fnessref  31084  topmeet  31091  topjoin  31092  neifg  31098  relowlssretop  31836  fin2solem  31995  fin2so  31996  poimirlem4  32008  poimirlem25  32029  poimirlem26  32030  poimirlem27  32031  poimirlem31  32035  poimirlem32  32036  opnmbllem0  32040  mblfinlem2  32042  itg2gt0cn  32061  indexa  32124  nninfnub  32144  istotbnd  32165  sstotbnd2  32170  isbnd  32176  isrngohom  32268  isrngoiso  32281  isidl  32311  ispridl  32331  ismaxidl  32337  prnc  32364  isfldidl  32365  islshp  32616  lssats  32649  islfl  32697  isat  32923  atlatmstc  32956  islln  33142  islpln  33166  islvol  33209  linepsubN  33388  elpmap  33394  pmapsub  33404  elpadd  33435  paddvaln0N  33437  islhp  33632  isldil  33746  isltrn  33755  isdilN  33791  istrnN  33794  diaval  34671  diaelval  34672  diaeldm  34675  diaelrnN  34684  cdlemm10N  34757  docaclN  34763  dibglbN  34805  dicval  34815  dicfnN  34822  dicvalrelN  34824  dihglblem2aN  34932  dihglblem2N  34933  dihglblem3N  34934  dih1dimatlem  34968  dihglb2  34981  dochvalr  34996  doch2val2  35003  dochocss  35005  islpolN  35122  mapd0  35304  isnacs  35617  elmzpcl  35639  mzpindd  35659  rencldnfilem  35734  irrapxlem6  35742  pellexlem3  35746  pellexlem5  35748  elpell1qr  35764  elpell14qr  35766  elpell1234qr  35768  pellfundre  35800  pellfundge  35801  pellfundlb  35803  pellfundglb  35804  rmspecnonsq  35826  jm2.22  35921  jm2.23  35922  rpnnen3lem  35957  fnwe2lem2  35980  fnwe2lem3  35981  elmnc  36066  dgraalem  36078  dgraalemOLD  36079  dgraaub  36084  dgraaubOLD  36085  mpaalem  36089  rgspnmin  36108  issdrg  36134  phisum  36147  nzss  36736  iccshift  37715  iooshift  37719  limcperiod  37805  sumnnodd  37807  ioodvbdlimc1lem1  37900  ioodvbdlimc1lem1OLD  37902  dvnprodlem1  37918  dvnprodlem3  37920  itgperiod  37955  stoweidlem14  37986  stoweidlem15  37987  stoweidlem16  37988  stoweidlem31  38004  stoweidlem36  38009  stoweidlem46  38019  stoweidlem48  38021  fourierdlem2  38083  fourierdlem3  38084  fourierdlem20  38101  fourierdlem25  38106  fourierdlem37  38119  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem48  38130  fourierdlem51  38133  fourierdlem63  38145  fourierdlem64  38146  fourierdlem65  38147  fourierdlem79  38161  fourierdlem81  38163  elaa2lem  38209  elaa2lemOLD  38210  etransclem24  38235  etransclem26  38237  etransclem28  38239  etransclem35  38246  etransclem48OLD  38259  etransclem48  38260  salgenval  38294  salgenn0  38302  salgencl  38303  sssalgen  38306  salgenss  38307  salgenuni  38308  issalgend  38309  salgencntex  38314  sge0fodjrnlem  38372  meadjiunlem  38419  caragenel  38435  ovnlecvr  38498  ovnpnfelsup  38499  ovncvrrp  38504  ovnsubaddlem1  38510  hoidmv1lelem1  38531  hoidmv1lelem2  38532  hoidmv1lelem3  38533  hoidmvlelem1  38535  hoidmvlelem2  38536  hoidmvlelem4  38538  ovnhoilem1  38541  ovnlecvr2  38550  ovncvr2  38551  iccpart  38875  iseven  38902  isodd  38903  dfodd2  38911  dfeven5  38941  dfodd7  38942  upgrle  39336  upgrbi  39339  umgredg2  39345  umgrbi  39346  upgr1elem  39357  edgupgr  39386  edgumgr  39387  upgredg  39389  edgusgr  39409  usgruspgrb  39429  usgredg2ALT  39438  ushgredgedga  39470  ushgredgedgaloop  39472  subumgredg2  39521  subupgr  39523  upgrres1  39544  nbgrel  39574  nbupgrel  39577  nbumgrvtx  39578  nbusgreledg  39585  nbgrnself  39593  nbusgredgeu0  39606  nbusgrf1o0  39607  uvtxael  39624  uvtxael1  39632  uvtxusgrel  39640  1hevtxdg1  39728  1hegrlfgr  39729  umgr2v2e  39748  rgrusgrprc  39793  rgrx0ndm  39797  lfgrwlkprop  39879  eupth2lems  40150  konigsberglem4  40169  ismgmhm  40291  issubmgm  40297  rabsubmgmd  40299  mgmhmeql  40311  assintop  40353  isassintop  40354  assintopcllaw  40356  isrnghm  40400  isrngisom  40404  0even  40439  2even  40441  2zrngamgm  40447  dmatALTbasel  40703  lcoval  40713  elbigo  40870  secval  40975  cscval  40976  cotval  40977
  Copyright terms: Public domain W3C validator