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

Theorem elrab 2923
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 2419 . 2  |-  F/_ x A
2 nfcv 2419 . 2  |-  F/_ x B
3 nfv 1605 . 2  |-  F/ x ps
4 elrab.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
51, 2, 3, 4elrabf 2922 1  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623    e. wcel 1684   {crab 2547
This theorem is referenced by:  elrab3  2924  elrab2  2925  ralrab  2927  rexrab  2929  rabsnt  3704  unimax  3861  ssintub  3880  intminss  3888  reusv6OLD  4545  rabxfrd  4555  onnminsb  4595  dfom2  4658  ssnlim  4674  ssimaex  5584  weniso  5852  sorpsscmpl  6288  canth  6294  oeeulem  6599  nnawordex  6635  elpmg  6786  fineqvlem  7077  supub  7210  suplub  7211  ordtypelem6  7238  ordtypelem7  7239  hartogslem1  7257  hartogs  7259  wemapso2lem  7265  card2on  7268  elharval  7277  wdom2d  7294  cantnfs  7367  oemapvali  7386  rankuni2b  7525  scottex  7555  tskwe  7583  cardid2  7586  iscard2  7609  harval2  7630  cardmin2  7631  acni3  7674  alephsuc2  7707  kmlem1  7776  cofsmo  7895  coftr  7899  fin23lem11  7943  enfin2i  7947  fin1a2lem9  8034  fin1a2lem11  8036  axcc4  8065  axdc3lem2  8077  zorn2lem7  8129  ondomon  8185  alephval2  8194  grutsk  8444  pinq  8551  infm3  9713  infmrcl  9733  nnind  9764  peano2uz2  10099  peano5uzi  10100  dfuzi  10102  uzind  10103  uzind3  10105  uzind3OLD  10107  eluz1  10234  uzind4  10276  nnwos  10286  eqreznegel  10303  supminf  10305  zsupss  10307  zmin  10312  elixx1  10665  elioo2  10697  elfz1  10787  flval3  10945  serge0  11100  expge0  11138  expge1  11139  hashbclem  11390  shftf  11574  rlimrege0  12053  incexc2  12297  divalglem4  12595  divalgmod  12605  bitsval  12615  sadval  12647  smuval  12672  bezout  12721  1nprm  12763  1idssfct  12764  isprm2  12766  phicl2  12836  hashdvds  12843  odzval  12856  odzcllem  12857  odzdvds  12860  pcpremul  12896  prmreclem1  12963  prmreclem2  12964  prmreclem3  12965  prmreclem5  12967  ramub  13060  rami  13062  ramub1lem1  13073  ramub1lem2  13074  ismre  13492  mrcflem  13508  mrcval  13512  ismri  13533  isacs  13553  isacs1i  13559  catlid  13585  catrid  13586  ismon  13636  isnat  13821  eldmcoa  13897  coaval  13900  ismhm  14417  issubm  14425  mhmeql  14441  gsumress  14454  gsumval2  14460  grplinv  14528  issubg  14621  cycsubg  14645  isnsg  14646  ghmeql  14705  isgim  14726  isga  14745  elcntz  14798  elcntzsn  14801  odid  14853  odlem2  14854  gexid  14892  gexlem2  14893  gexdvds  14895  isslw  14919  pgpssslw  14925  pj1id  15008  efgsfo  15048  oddvdssubg  15147  pgpfac1lem5  15314  ablfaclem2  15321  isirred  15481  issubrg  15545  isabv  15584  islss  15692  islmhm  15784  lmhmeql  15812  islmim  15815  islbs  15829  gsumbagdiaglem  16121  psrmulcllem  16132  psrlidm  16148  psrridm  16149  psrass1  16150  psrcom  16153  mplsubglem  16179  mpllsslem  16180  mplmonmul  16208  coe1mul2  16346  elocv  16568  isobs  16620  istopon  16663  fctop  16741  cctop  16743  ppttop  16744  pptbas  16745  epttop  16746  iscld  16764  clscld  16784  isnei  16840  neips  16850  iscn  16965  iscnp  16967  ordthauslem  17111  cmpsublem  17126  concompcon  17158  2ndc1stc  17177  2ndcdisj  17182  elkgen  17231  xkoopn  17284  xkoccn  17313  txdis1cn  17329  pthaus  17332  txkgen  17346  xkohaus  17347  xkococnlem  17353  xkococn  17354  xkoinjcn  17381  txcon  17383  elqtop  17388  nrmr0reg  17440  elmptrab  17522  fbssfi  17532  opnfbas  17537  elfg  17566  cfinfil  17588  csdfil  17589  supfil  17590  filssufilg  17606  uffix  17616  fixufil  17617  uffixfr  17618  uffixsn  17620  ufinffr  17624  ufilen  17625  elflim2  17659  supnfcls  17715  fclscf  17720  flimfnfcls  17723  alexsubALTlem2  17742  alexsubALTlem4  17744  alexsubALT  17745  ptcmplem2  17747  tmdgsum2  17779  symgtgp  17784  ghmcnp  17797  ismet  17888  isxmet  17889  elbl  17949  icccmp  18330  elcncf  18393  ishtpy  18470  isphtpy  18479  om1elbas  18530  iscfil  18691  iscau  18702  iscmet  18710  lmle  18727  minveclem3  18793  minveclem4  18796  ovolshftlem1  18868  ovolscalem1  18872  ovolicc2lem3  18878  iundisj  18905  dyadmax  18953  dyadmbllem  18954  opnmbllem  18956  vitalilem2  18964  vitalilem3  18965  elcpn  19283  evlsval2  19404  ig1pval3  19560  coelem  19608  quotlem  19680  elqaalem1  19699  elqaalem3  19701  aannenlem1  19708  aannenlem2  19709  aalioulem2  19713  radcnv0  19792  dmarea  20252  jensen  20283  ftalem4  20313  ftalem5  20314  efnnfsumcl  20340  efchtdvds  20397  sqff1o  20420  dvdsdivcl  20421  fsumdvdsdiaglem  20423  dvdsppwf1o  20426  dvdsflf1o  20427  dvdsflsumcom  20428  musum  20431  muinv  20433  logfac2  20456  dchrelbas  20475  dchrfi  20494  lgsfle1  20544  lgsle1  20550  lgsdirprm  20568  lgsne0  20572  lgsquadlem1  20593  lgsquadlem2  20594  dchrvmasumlem1  20644  logsqvma  20691  pntleml  20760  grpoidinv2  20885  grpoinv  20894  isssp  21300  islno  21331  isblo  21360  ishmo  21389  ubthlem1  21449  ubthlem2  21450  htthlem  21497  ocel  21860  shsval2i  21966  ococin  21987  chsupsn  21992  eleigvec  22537  cnlnadjlem5  22651  shatomistici  22941  hatomistici  22942  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemiex  23060  ballotlemfrcn0  23088  ballotlemirc  23090  ballotlem7  23094  sigagenval  23501  sigagenss  23510  ismbfm  23557  imambfm  23567  indf1ofs  23609  dstfrvel  23674  conpcon  23766  iscvm  23790  cvmsi  23796  cvmsval  23797  cvmliftmolem2  23813  cvmliftiota  23832  umgrale  23873  umgra1  23878  eupath2  23904  umgrabi  23907  konigsberg  23911  snmlval  23914  elgiso  24003  sltval2  24310  sltres  24318  nodenselem7  24341  nofulllem5  24360  lineelsb2  24771  linerflx1  24772  rankeq1o  24801  dstr  25171  puub2  25258  puub  25259  supdef  25262  ismxl2  25267  ismnl2  25268  isidlNEW  25446  usptoplem  25546  usptop  25550  prcnt  25551  fgsb2  25555  iint  25612  ishomc  25789  ismonb  25810  isepib  25820  cinvlem3  25830  isfunb  25835  issrc  25867  propsrc  25868  isntr  25873  islimcat  25876  isnword  25986  isconcl2b  26098  isibcg  26191  finminlem  26231  fneint  26277  fnessref  26293  locfincmp  26304  topmeet  26313  topjoin  26314  neifg  26320  indexa  26412  nninfnub  26461  istotbnd  26493  sstotbnd2  26498  isbnd  26504  isrngohom  26596  isrngoiso  26609  isidl  26639  ispridl  26659  ismaxidl  26665  prnc  26692  isfldidl  26693  isnacs  26779  elmzpcl  26804  mzpindd  26824  rencldnfilem  26903  irrapxlem6  26912  pellexlem3  26916  pellexlem5  26918  elpell1qr  26932  elpell14qr  26934  elpell1234qr  26936  pellfundre  26966  pellfundge  26967  pellfundlb  26969  pellfundglb  26970  rmspecnonsq  26992  jm2.22  27088  jm2.23  27089  rpnnen3lem  27124  fnwe2lem2  27148  fnwe2lem3  27149  dsmmelbas  27205  frlmelbas  27224  frlmssuvc2  27247  islinds  27279  elmnc  27341  dgraalem  27350  dgraaub  27353  mpaalem  27357  rgspnmin  27376  issubmd  27383  pmtrval  27394  pmtrrn  27399  symgsssg  27408  symgfisg  27409  psgnunilem5  27417  issdrg  27505  phisum  27518  stoweidlem14  27763  stoweidlem15  27764  stoweidlem31  27780  stoweidlem36  27785  stoweidlem37  27786  stoweidlem46  27795  stoweidlem48  27797  stoweidlem51  27800  uslgra1  28118  usgra1  28119  usgraedg2  28121  usgraedgrnv  28123  usgraexmpl  28133  nbgrael  28141  nbgraeledg  28145  nbcusgra  28159  uvtxel  28161  uvtxisvtx  28162  uvtxnbgra  28165  cusgrauvtx  28168  secval  28217  cscval  28218  cotval  28219  islshp  29169  lssats  29202  islfl  29250  isat  29476  atlatmstc  29509  islln  29695  islpln  29719  islvol  29762  linepsubN  29941  elpmap  29947  pmapsub  29957  elpadd  29988  paddvaln0N  29990  islhp  30185  isldil  30299  isltrn  30308  isdilN  30343  istrnN  30346  diaval  31222  diaelval  31223  diaeldm  31226  diaelrnN  31235  cdlemm10N  31308  docaclN  31314  dibglbN  31356  dicval  31366  dicfnN  31373  dicvalrelN  31375  dihglblem2aN  31483  dihglblem2N  31484  dihglblem3N  31485  dih1dimatlem  31519  dihglb2  31532  dochvalr  31547  doch2val2  31554  dochocss  31556  islpolN  31673  mapd0  31855
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790
  Copyright terms: Public domain W3C validator