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

Theorem elrab 3261
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 2629 . 2  |-  F/_ x A
2 nfcv 2629 . 2  |-  F/_ x B
3 nfv 1683 . 2  |-  F/ x ps
4 elrab.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
51, 2, 3, 4elrabf 3259 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 1379    e. wcel 1767   {crab 2818
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115
This theorem is referenced by:  elrab3  3262  elrab2  3263  ralrab  3265  rexrab  3267  rabsnt  4104  unimax  4281  ssintub  4300  intminss  4308  reusv6OLD  4658  rabxfrd  4668  ssimaex  5930  weniso  6236  canth  6240  sorpsscmpl  6573  onnminsb  6617  dfom2  6680  ssnlim  6696  elsuppfn  6906  ressuppssdif  6918  oeeulem  7247  nnawordex  7283  elpmg  7431  fineqvlem  7731  mapfienlem2  7861  supub  7915  suplub  7916  ordtypelem6  7944  ordtypelem7  7945  hartogslem1  7963  hartogs  7965  wemapsolem  7971  card2on  7976  elharval  7985  wdom2d  8002  cantnfs  8081  oemapvali  8099  cantnfsOLD  8111  rankuni2b  8267  scottex  8299  tskwe  8327  cardid2  8330  iscard2  8353  harval2  8374  cardmin2  8375  acni3  8424  alephsuc2  8457  kmlem1  8526  cofsmo  8645  coftr  8649  fin23lem11  8693  enfin2i  8697  fin1a2lem9  8784  fin1a2lem11  8786  axcc4  8815  axdc3lem2  8827  zorn2lem7  8878  ondomon  8934  alephval2  8943  grutsk  9196  pinq  9301  infm3  10498  infmrcl  10518  nnind  10550  peano2uz2  10944  peano5uzi  10945  dfuzi  10947  uzind  10948  uzind3  10950  uzind3OLD  10952  eluz1  11082  uzind4  11135  nnwos  11145  eqreznegel  11163  zsupss  11167  zmin  11174  elixx1  11534  elioo2  11566  elfz1  11673  flval3  11914  serge0  12124  expge0  12164  expge1  12165  hashbclem  12461  pr2pwpr  12480  elss2pr  12487  disjxwrd  12637  wwlktovf  12851  wwlktovf1  12852  wwlktovfo  12853  shftf  12869  rlimrege0  13358  incexc2  13606  divalglem4  13906  divalgmod  13916  bitsval  13926  bezout  14032  1nprm  14074  1idssfct  14075  isprm2  14077  phicl2  14150  hashdvds  14157  odzval  14170  odzcllem  14171  odzdvds  14174  pcpremul  14219  prmreclem1  14286  prmreclem2  14287  prmreclem3  14288  prmreclem5  14290  ramub  14383  rami  14385  ramub1lem1  14396  ramub1lem2  14397  ismre  14838  mrcflem  14854  mrcval  14858  ismri  14879  isacs  14899  isacs1i  14905  catlid  14931  catrid  14932  ismon  14982  isnat  15167  eldmcoa  15243  coaval  15246  lubeldm  15461  glbeldm  15474  ismhm  15776  issubm  15785  issubmd  15787  mhmeql  15802  mrcmndind  15804  gsumress  15817  gsumval2  15823  grplinv  15894  issubg  15993  cycsubg  16021  isnsg  16022  ghmeql  16081  isgim  16102  isga  16121  elcntz  16152  elcntzsn  16155  symgfix2  16233  pmtrval  16269  pmtrrn  16275  symgsssg  16285  symgfisg  16286  psgnunilem5  16312  odid  16355  odlem2  16356  gexid  16394  gexlem2  16395  gexdvds  16397  isslw  16421  pgpssslw  16427  pj1id  16510  efgsfo  16550  oddvdssubg  16651  pgpfac1lem5  16917  ablfaclem2  16924  isirred  17129  isrim0  17153  issubrg  17209  isabv  17248  islss  17361  islmhm  17453  lmhmeql  17481  islmim  17488  islbs  17502  gsumbagdiaglem  17795  psrmulcllem  17808  psrlidm  17824  psrlidmOLD  17825  psrridm  17826  psrridmOLD  17827  psrass1  17828  psrcom  17832  mplsubglem  17861  mpllsslem  17862  mplsubglemOLD  17863  mpllsslemOLD  17864  mplmonmul  17894  evlsval2  17957  coe1fsupp  18022  coe1ae0  18025  coe1mul2  18078  zrhcofipsgn  18393  psgndiflemB  18400  elocv  18463  isobs  18515  dsmmelbas  18534  frlmelbas  18552  frlmelbasOLD  18553  frlmssuvc2  18590  frlmssuvc2OLD  18592  islinds  18608  dmatel  18759  dmatmulcl  18766  scmatel  18771  scmateALT  18778  symgmatr01lem  18919  pmatcoe1fsupp  18966  cpmatel  18976  chpscmat  19107  istopon  19190  fctop  19268  cctop  19270  ppttop  19271  pptbas  19272  epttop  19273  iscld  19291  clscld  19311  isnei  19367  neips  19377  neiptopnei  19396  iscn  19499  iscnp  19501  ordthauslem  19647  cmpsublem  19662  concompcon  19696  2ndc1stc  19715  2ndcdisj  19720  elkgen  19769  xkoopn  19822  xkoccn  19852  txdis1cn  19868  pthaus  19871  txkgen  19885  xkohaus  19886  xkococnlem  19892  xkococn  19893  xkoinjcn  19920  txcon  19922  elqtop  19930  nrmr0reg  19982  elmptrab  20060  fbssfi  20070  opnfbas  20075  elfg  20104  cfinfil  20126  csdfil  20127  supfil  20128  filssufilg  20144  uffix  20154  fixufil  20155  uffixfr  20156  uffixsn  20158  ufinffr  20162  ufilen  20163  elflim2  20197  supnfcls  20253  fclscf  20258  flimfnfcls  20261  alexsubALTlem2  20280  alexsubALTlem4  20282  alexsubALT  20283  ptcmplem2  20285  tmdgsum2  20327  symgtgp  20332  ghmcnp  20345  elutop  20468  isucn  20513  iscfilu  20523  ispsmet  20540  ismet  20558  isxmet  20559  elblps  20622  elbl  20623  restmetu  20822  icccmp  21062  elcncf  21125  ishtpy  21204  isphtpy  21213  om1elbas  21264  iscfil  21436  iscau  21447  iscmet  21455  lmle  21472  rrxfsupp  21561  minveclem3  21576  minveclem4  21579  ovolshftlem1  21652  ovolscalem1  21656  ovolicc2lem3  21662  iundisj  21690  dyadmax  21739  dyadmbllem  21740  opnmbllem  21742  vitalilem2  21750  vitalilem3  21751  elcpn  22069  ig1pval3  22307  coelem  22355  quotlem  22427  elqaalem1  22446  elqaalem3  22448  aannenlem1  22455  aannenlem2  22456  aalioulem2  22460  radcnv0  22542  dmarea  23012  jensen  23043  ftalem4  23074  ftalem5  23075  efnnfsumcl  23101  efchtdvds  23158  sqff1o  23181  dvdsdivcl  23182  fsumdvdsdiaglem  23184  dvdsppwf1o  23187  dvdsflf1o  23188  dvdsflsumcom  23189  musum  23192  muinv  23194  logfac2  23217  dchrelbas  23236  dchrfi  23255  lgsfle1  23305  lgsle1  23311  lgsdirprm  23329  lgsne0  23333  lgsquadlem1  23354  lgsquadlem2  23355  dchrvmasumlem1  23405  logsqvma  23452  pntleml  23521  tgellng  23665  mircgr  23748  mirbtwn  23749  ttgelitv  23859  ebtwntg  23958  umgrale  23994  umgra1  23999  uslgra1  24045  usgra1  24046  usgraedg2  24048  usgraedgrnv  24050  usgrarnedg  24057  usgraedg4  24060  usgraexmpl  24074  usgrares1  24083  nbgrael  24099  nbgraeledg  24103  nbgraf1olem3  24116  cusgrarn  24132  nbcusgra  24136  cusgrares  24145  uvtxel  24162  uvtxnbgra  24166  cusgrauvtxb  24169  iswwlk  24356  iswwlkn  24357  wlknwwlknsur  24385  wlkiswwlksur  24392  wwlkextinj  24403  wwlkextsur  24404  wlknwwlknvbij  24413  isclwwlk  24441  isclwwlkn  24442  clwwlkprop  24443  clwwlknprop  24445  clwwlkvbij  24474  clwwlknscsh  24492  eleclclwwlkn  24506  clwlkfclwwlk1hashn  24514  clwlkf1clwwlklem1  24519  clwlkf1clwwlklem2  24520  el2wlkonot  24542  el2spthonot  24543  el2spthonot0  24544  el2wlksoton  24551  el2spthsoton  24552  el2wlksotot  24555  rusgranumwlklem0  24621  rusgranumwlklem1  24622  rusgranumwlklem3  24624  rusgranumwlks  24629  eupath2  24653  umgrabi  24656  konigsberg  24660  2spotdisj  24735  usg2spot2nb  24739  usgreg2spot  24741  numclwwlkun  24753  numclwwlkovfel2  24757  numclwwlkovgel  24762  numclwlk1lem2foa  24765  numclwwlk2lem1  24776  numclwlk2lem2f  24777  numclwlk2lem2f1o  24779  grpoidinv2  24893  grpoinv  24902  isssp  25310  islno  25341  isblo  25370  ishmo  25399  ubthlem1  25459  ubthlem2  25460  htthlem  25507  ocel  25872  shsval2i  25978  ococin  25999  chsupsn  26004  eleigvec  26549  cnlnadjlem5  26663  shatomistici  26953  hatomistici  26954  nnindf  27275  ordtconlem1  27539  indf1ofs  27676  sigagenval  27777  ddemeas  27845  ismbfm  27860  imambfm  27870  dya2iocuni  27891  oms0  27903  issibf  27912  sitgfval  27920  oddpwdc  27930  eulerpartlemgh  27954  eulerpartlemgs2  27956  dstfrvel  28049  ballotlemfc0  28068  ballotlemfcc  28069  ballotlemiex  28077  ballotlemfrcn0  28105  ballotlemirc  28107  ballotlem7  28111  conpcon  28317  iscvm  28341  cvmsi  28347  cvmsval  28348  cvmliftmolem2  28364  cvmliftiota  28383  snmlval  28413  elgiso  28508  sltval2  28990  sltres  28998  nodenselem7  29021  nofulllem5  29040  lineelsb2  29372  linerflx1  29373  rankeq1o  29402  fin2solem  29613  fin2so  29614  opnmbllem0  29625  mblfinlem2  29627  itg2gt0cn  29645  finminlem  29711  fneint  29747  fnessref  29763  locfincmp  29774  topmeet  29783  topjoin  29784  neifg  29790  indexa  29825  nninfnub  29845  istotbnd  29866  sstotbnd2  29871  isbnd  29877  isrngohom  29969  isrngoiso  29982  isidl  30012  ispridl  30032  ismaxidl  30038  prnc  30065  isfldidl  30066  isnacs  30238  elmzpcl  30260  mzpindd  30280  rencldnfilem  30356  irrapxlem6  30365  pellexlem3  30369  pellexlem5  30371  elpell1qr  30385  elpell14qr  30387  elpell1234qr  30389  pellfundre  30419  pellfundge  30420  pellfundlb  30422  pellfundglb  30423  rmspecnonsq  30445  jm2.22  30541  jm2.23  30542  rpnnen3lem  30577  fnwe2lem2  30601  fnwe2lem3  30602  elmnc  30690  dgraalem  30699  dgraaub  30702  mpaalem  30706  rgspnmin  30725  issdrg  30751  phisum  30764  lcmledvds  30805  lcmgcdlem  30812  nzss  30822  iccshift  31122  iooshift  31126  limcperiod  31170  sumnnodd  31172  ioodvbdlimc1lem1  31261  itgiccshift  31298  itgperiod  31299  stoweidlem14  31314  stoweidlem15  31315  stoweidlem16  31316  stoweidlem31  31331  stoweidlem36  31336  stoweidlem46  31346  stoweidlem48  31348  fourierdlem2  31409  fourierdlem3  31410  fourierdlem20  31427  fourierdlem25  31432  fourierdlem37  31444  fourierdlem42  31449  fourierdlem45  31452  fourierdlem48  31455  fourierdlem51  31458  fourierdlem63  31470  fourierdlem64  31471  fourierdlem65  31472  fourierdlem79  31486  fourierdlem81  31488  assintop  31956  dmatALTbasel  32076  lcoval  32086  secval  32222  cscval  32223  cotval  32224  islshp  33776  lssats  33809  islfl  33857  isat  34083  atlatmstc  34116  islln  34302  islpln  34326  islvol  34369  linepsubN  34548  elpmap  34554  pmapsub  34564  elpadd  34595  paddvaln0N  34597  islhp  34792  isldil  34906  isltrn  34915  isdilN  34950  istrnN  34953  diaval  35829  diaelval  35830  diaeldm  35833  diaelrnN  35842  cdlemm10N  35915  docaclN  35921  dibglbN  35963  dicval  35973  dicfnN  35980  dicvalrelN  35982  dihglblem2aN  36090  dihglblem2N  36091  dihglblem3N  36092  dih1dimatlem  36126  dihglb2  36139  dochvalr  36154  doch2val2  36161  dochocss  36163  islpolN  36280  mapd0  36462
  Copyright terms: Public domain W3C validator