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

Theorem elrab 3092
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 2572 . 2  |-  F/_ x A
2 nfcv 2572 . 2  |-  F/_ x B
3 nfv 1629 . 2  |-  F/ x ps
4 elrab.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
51, 2, 3, 4elrabf 3091 1  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1652    e. wcel 1725   {crab 2709
This theorem is referenced by:  elrab3  3093  elrab2  3094  ralrab  3096  rexrab  3098  rabsnt  3881  unimax  4049  ssintub  4068  intminss  4076  reusv6OLD  4734  rabxfrd  4744  onnminsb  4784  dfom2  4847  ssnlim  4863  ssimaex  5788  weniso  6075  sorpsscmpl  6533  canth  6539  oeeulem  6844  nnawordex  6880  elpmg  7032  fineqvlem  7323  supub  7464  suplub  7465  ordtypelem6  7492  ordtypelem7  7493  hartogslem1  7511  hartogs  7513  wemapso2lem  7519  card2on  7522  elharval  7531  wdom2d  7548  cantnfs  7621  oemapvali  7640  rankuni2b  7779  scottex  7809  tskwe  7837  cardid2  7840  iscard2  7863  harval2  7884  cardmin2  7885  acni3  7928  alephsuc2  7961  kmlem1  8030  cofsmo  8149  coftr  8153  fin23lem11  8197  enfin2i  8201  fin1a2lem9  8288  fin1a2lem11  8290  axcc4  8319  axdc3lem2  8331  zorn2lem7  8382  ondomon  8438  alephval2  8447  grutsk  8697  pinq  8804  infm3  9967  infmrcl  9987  nnind  10018  peano2uz2  10357  peano5uzi  10358  dfuzi  10360  uzind  10361  uzind3  10363  uzind3OLD  10365  eluz1  10492  uzind4  10534  nnwos  10544  eqreznegel  10561  zsupss  10565  zmin  10570  elixx1  10925  elioo2  10957  elfz1  11048  flval3  11222  serge0  11377  expge0  11416  expge1  11417  hashbclem  11701  shftf  11894  rlimrege0  12373  incexc2  12618  divalglem4  12916  divalgmod  12926  bitsval  12936  bezout  13042  1nprm  13084  1idssfct  13085  isprm2  13087  phicl2  13157  hashdvds  13164  odzval  13177  odzcllem  13178  odzdvds  13181  pcpremul  13217  prmreclem1  13284  prmreclem2  13285  prmreclem3  13286  prmreclem5  13288  ramub  13381  rami  13383  ramub1lem1  13394  ramub1lem2  13395  ismre  13815  mrcflem  13831  mrcval  13835  ismri  13856  isacs  13876  isacs1i  13882  catlid  13908  catrid  13909  ismon  13959  isnat  14144  eldmcoa  14220  coaval  14223  ismhm  14740  issubm  14748  mhmeql  14764  gsumress  14777  gsumval2  14783  grplinv  14851  issubg  14944  cycsubg  14968  isnsg  14969  ghmeql  15028  isgim  15049  isga  15068  elcntz  15121  elcntzsn  15124  odid  15176  odlem2  15177  gexid  15215  gexlem2  15216  gexdvds  15218  isslw  15242  pgpssslw  15248  pj1id  15331  efgsfo  15371  oddvdssubg  15470  pgpfac1lem5  15637  ablfaclem2  15644  isirred  15804  issubrg  15868  isabv  15907  islss  16011  islmhm  16103  lmhmeql  16131  islmim  16134  islbs  16148  gsumbagdiaglem  16440  psrmulcllem  16451  psrlidm  16467  psrridm  16468  psrass1  16469  psrcom  16472  mplsubglem  16498  mpllsslem  16499  mplmonmul  16527  coe1mul2  16662  elocv  16895  isobs  16947  istopon  16990  fctop  17068  cctop  17070  ppttop  17071  pptbas  17072  epttop  17073  iscld  17091  clscld  17111  isnei  17167  neips  17177  neiptopnei  17196  iscn  17299  iscnp  17301  ordthauslem  17447  cmpsublem  17462  concompcon  17495  2ndc1stc  17514  2ndcdisj  17519  elkgen  17568  xkoopn  17621  xkoccn  17651  txdis1cn  17667  pthaus  17670  txkgen  17684  xkohaus  17685  xkococnlem  17691  xkococn  17692  xkoinjcn  17719  txcon  17721  elqtop  17729  nrmr0reg  17781  elmptrab  17859  fbssfi  17869  opnfbas  17874  elfg  17903  cfinfil  17925  csdfil  17926  supfil  17927  filssufilg  17943  uffix  17953  fixufil  17954  uffixfr  17955  uffixsn  17957  ufinffr  17961  ufilen  17962  elflim2  17996  supnfcls  18052  fclscf  18057  flimfnfcls  18060  alexsubALTlem2  18079  alexsubALTlem4  18081  alexsubALT  18082  ptcmplem2  18084  tmdgsum2  18126  symgtgp  18131  ghmcnp  18144  elutop  18263  isucn  18308  iscfilu  18318  ispsmet  18335  ismet  18353  isxmet  18354  elblps  18417  elbl  18418  restmetu  18617  icccmp  18856  elcncf  18919  ishtpy  18997  isphtpy  19006  om1elbas  19057  iscfil  19218  iscau  19229  iscmet  19237  lmle  19254  minveclem3  19330  minveclem4  19333  ovolshftlem1  19405  ovolscalem1  19409  ovolicc2lem3  19415  iundisj  19442  dyadmax  19490  dyadmbllem  19491  opnmbllem  19493  vitalilem2  19501  vitalilem3  19502  elcpn  19820  evlsval2  19941  ig1pval3  20097  coelem  20145  quotlem  20217  elqaalem1  20236  elqaalem3  20238  aannenlem1  20245  aannenlem2  20246  aalioulem2  20250  radcnv0  20332  dmarea  20796  jensen  20827  ftalem4  20858  ftalem5  20859  efnnfsumcl  20885  efchtdvds  20942  sqff1o  20965  dvdsdivcl  20966  fsumdvdsdiaglem  20968  dvdsppwf1o  20971  dvdsflf1o  20972  dvdsflsumcom  20973  musum  20976  muinv  20978  logfac2  21001  dchrelbas  21020  dchrfi  21039  lgsfle1  21089  lgsle1  21095  lgsdirprm  21113  lgsne0  21117  lgsquadlem1  21138  lgsquadlem2  21139  dchrvmasumlem1  21189  logsqvma  21236  pntleml  21305  umgrale  21356  umgra1  21361  uslgra1  21392  usgra1  21393  usgraedg2  21395  usgraedgrnv  21397  usgrarnedg  21404  usgraedg4  21406  usgraexmpl  21420  usgrares1  21424  nbgrael  21438  nbgraeledg  21442  nbgraf1olem3  21453  cusgrarn  21468  nbcusgra  21472  cusgrares  21481  uvtxel  21498  uvtxnbgra  21502  cusgrauvtxb  21505  eupath2  21702  umgrabi  21705  konigsberg  21709  grpoidinv2  21806  grpoinv  21815  isssp  22223  islno  22254  isblo  22283  ishmo  22312  ubthlem1  22372  ubthlem2  22373  htthlem  22420  ocel  22783  shsval2i  22889  ococin  22910  chsupsn  22915  eleigvec  23460  cnlnadjlem5  23574  shatomistici  23864  hatomistici  23865  indf1ofs  24423  sigagenval  24523  ismbfm  24602  imambfm  24612  dya2iocuni  24633  issibf  24648  sitgfval  24655  dstfrvel  24731  ballotlemfc0  24750  ballotlemfcc  24751  ballotlemiex  24759  ballotlemfrcn0  24787  ballotlemirc  24789  ballotlem7  24793  conpcon  24922  iscvm  24946  cvmsi  24952  cvmsval  24953  cvmliftmolem2  24969  cvmliftiota  24988  snmlval  25018  elgiso  25107  sltval2  25611  sltres  25619  nodenselem7  25642  nofulllem5  25661  lineelsb2  26082  linerflx1  26083  rankeq1o  26112  opnmbllem0  26242  mblfinlem2  26244  itg2gt0cn  26260  finminlem  26321  fneint  26357  fnessref  26373  locfincmp  26384  topmeet  26393  topjoin  26394  neifg  26400  indexa  26435  nninfnub  26455  istotbnd  26478  sstotbnd2  26483  isbnd  26489  isrngohom  26581  isrngoiso  26594  isidl  26624  ispridl  26644  ismaxidl  26650  prnc  26677  isfldidl  26678  isnacs  26758  elmzpcl  26783  mzpindd  26803  rencldnfilem  26881  irrapxlem6  26890  pellexlem3  26894  pellexlem5  26896  elpell1qr  26910  elpell14qr  26912  elpell1234qr  26914  pellfundre  26944  pellfundge  26945  pellfundlb  26947  pellfundglb  26948  rmspecnonsq  26970  jm2.22  27066  jm2.23  27067  rpnnen3lem  27102  fnwe2lem2  27126  fnwe2lem3  27127  dsmmelbas  27182  frlmelbas  27201  frlmssuvc2  27224  islinds  27256  elmnc  27318  dgraalem  27327  dgraaub  27330  mpaalem  27334  rgspnmin  27353  issubmd  27360  pmtrval  27371  pmtrrn  27376  symgsssg  27385  symgfisg  27386  psgnunilem5  27394  issdrg  27482  phisum  27495  stoweidlem14  27739  stoweidlem15  27740  stoweidlem16  27741  stoweidlem31  27756  stoweidlem36  27761  stoweidlem46  27771  stoweidlem48  27773  el2wlkonot  28336  el2spthonot  28337  el2spthonot0  28338  el2wlksoton  28345  el2spthsoton  28346  el2wlksotot  28349  2spotdisj  28450  usg2spot2nb  28454  usgreg2spot  28456  secval  28490  cscval  28491  cotval  28492  islshp  29777  lssats  29810  islfl  29858  isat  30084  atlatmstc  30117  islln  30303  islpln  30327  islvol  30370  linepsubN  30549  elpmap  30555  pmapsub  30565  elpadd  30596  paddvaln0N  30598  islhp  30793  isldil  30907  isltrn  30916  isdilN  30951  istrnN  30954  diaval  31830  diaelval  31831  diaeldm  31834  diaelrnN  31843  cdlemm10N  31916  docaclN  31922  dibglbN  31964  dicval  31974  dicfnN  31981  dicvalrelN  31983  dihglblem2aN  32091  dihglblem2N  32092  dihglblem3N  32093  dih1dimatlem  32127  dihglb2  32140  dochvalr  32155  doch2val2  32162  dochocss  32164  islpolN  32281  mapd0  32463
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958
  Copyright terms: Public domain W3C validator