Theorem elrab 3363

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

Step	Hyp	Ref	Expression
1		nfcv 2764	. 2 |- F/_ x A
2		nfcv 2764	. 2 |- F/_ x B
3		nfv 1843	. 2 |- F/ x ps
4		elrab.1	. 2 |- ( x = A -> ( ph <-> ps ) )
5	1, 2, 3, 4	elrabf 3360	1 |- ( A e. { x e. B | ph } <-> ( A e. B /\ ps ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   {crab 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202

This theorem is referenced by:  elrab3  3364  elrabd  3365  elrab2  3366  ralrab  3368  rexrab  3370  rabsnt  4266  unimax  4473  ssintub  4495  intminss  4503  rabxfrd  4889  ssimaex  6263  weniso  6604  canth  6608  sorpsscmpl  6948  onnminsb  7004  dfom2  7067  ssnlim  7083  elsuppfn  7303  ressuppssdif  7316  oeeulem  7681  nnawordex  7717  elpmg  7873  fineqvlem  8174  mapfienlem2  8311  supub  8365  suplub  8366  ordtypelem6  8428  ordtypelem7  8429  hartogslem1  8447  hartogs  8449  wemapsolem  8455  card2on  8459  elharval  8468  wdom2d  8485  cantnfs  8563  oemapvali  8581  rankuni2b  8716  scottex  8748  tskwe  8776  cardid2  8779  iscard2  8802  harval2  8823  cardmin2  8824  acni3  8870  alephsuc2  8903  kmlem1  8972  cofsmo  9091  coftr  9095  fin23lem11  9139  enfin2i  9143  fin1a2lem9  9230  fin1a2lem11  9232  axcc4  9261  axdc3lem2  9273  zorn2lem7  9324  ondomon  9385  alephval2  9394  grutsk  9644  pinq  9749  negf1o  10460  fiminre  10972  infm3  10982  nnind  11038  peano2uz2  11465  peano5uzi  11466  dfuzi  11468  uzind  11469  uzind3  11471  eluz1  11691  uzind4  11746  nnwos  11755  eqreznegel  11774  zsupss  11777  zmin  11784  elixx1  12184  elioo2  12216  elfz1  12331  flval3  12616  serge0  12855  expge0  12896  expge1  12897  hashbclem  13236  pr2pwpr  13261  elss2prb  13269  hash2sspr  13270  wrdmap  13336  wwlktovfo  13701  shftf  13819  rlimrege0  14310  incexc2  14570  dvdsdivcl  15038  divalglem4  15119  divalgmod  15129  divalgmodOLD  15130  bitsval  15146  bezout  15260  dfgcd2  15263  lcmledvds  15312  lcmgcdlem  15319  lcmfledvds  15345  1nprm  15392  1idssfct  15393  isprm2  15395  phicl2  15473  hashdvds  15480  phisum  15495  odzval  15496  odzcllem  15497  odzdvds  15500  pcpremul  15548  prmreclem1  15620  prmreclem2  15621  prmreclem3  15622  prmreclem5  15624  ramub  15717  rami  15719  ramub1lem1  15730  ramub1lem2  15731  prmgaplem3  15757  prmgaplem4  15758  prmgaplem5  15759  prmgaplem6  15760  ismre  16250  mrcflem  16266  mrcval  16270  ismri  16291  isacs  16312  isacs1i  16318  catlid  16344  catrid  16345  ismon  16393  isnat  16607  eldmcoa  16715  coaval  16718  fncnvimaeqv  16760  lubeldm  16981  glbeldm  16994  gsumress  17276  gsumval2  17280  ismhm  17337  issubm  17347  issubmd  17349  mhmeql  17364  mrcmndind  17366  grplinv  17468  issubg  17594  cycsubg  17622  isnsg  17623  ghmeql  17683  isgim  17704  isga  17724  elcntz  17755  elcntzsn  17758  symgfix2  17836  pmtrval  17871  pmtrrn  17877  symgsssg  17887  symgfisg  17888  psgnunilem5  17914  odid  17957  odlem2  17958  gexid  17996  gexlem2  17997  gexdvds  17999  isslw  18023  pgpssslw  18029  pj1id  18112  efgsfo  18152  oddvdssubg  18258  dprdwd  18410  pgpfac1lem5  18478  ablfaclem2  18485  isirred  18699  isrim0  18723  issubrg  18780  isabv  18819  islss  18935  islmhm  19027  lmhmeql  19055  islmim  19062  islbs  19076  gsumbagdiaglem  19375  psrmulcllem  19387  psrlidm  19403  psrridm  19404  psrass1  19405  psrcom  19409  mplsubglem  19434  mpllsslem  19435  mplmonmul  19464  evlsval2  19520  coe1fsupp  19584  coe1ae0  19586  coe1mul2  19639  zrhcofipsgn  19939  psgndiflemB  19946  elocv  20012  isobs  20064  dsmmelbas  20083  frlmelbas  20100  frlmssuvc2  20134  islinds  20148  dmatel  20299  dmatmulcl  20306  scmatel  20311  scmateALT  20318  symgmatr01lem  20459  pmatcoe1fsupp  20506  cpmatel  20516  chpscmat  20647  istopon  20717  fctop  20808  cctop  20810  ppttop  20811  pptbas  20812  epttop  20813  iscld  20831  clscld  20851  isnei  20907  neips  20917  neiptopnei  20936  iscn  21039  iscnp  21041  ordthauslem  21187  cmpsublem  21202  conncompconn  21235  2ndc1stc  21254  2ndcdisj  21259  locfincmp  21329  elkgen  21339  xkoopn  21392  xkoccn  21422  txdis1cn  21438  pthaus  21441  txkgen  21455  xkohaus  21456  xkococnlem  21462  xkococn  21463  xkoinjcn  21490  txconn  21492  elqtop  21500  nrmr0reg  21552  elmptrab  21630  fbssfi  21641  opnfbas  21646  elfg  21675  cfinfil  21697  csdfil  21698  supfil  21699  filssufilg  21715  uffix  21725  fixufil  21726  uffixfr  21727  uffixsn  21729  ufinffr  21733  ufilen  21734  elflim2  21768  supnfcls  21824  fclscf  21829  flimfnfcls  21832  alexsubALTlem2  21852  alexsubALTlem4  21854  alexsubALT  21855  ptcmplem2  21857  tmdgsum2  21900  symgtgp  21905  ghmcnp  21918  elutop  22037  isucn  22082  iscfilu  22092  ispsmet  22109  ismet  22128  isxmet  22129  elblps  22192  elbl  22193  restmetu  22375  icccmp  22628  elcncf  22692  ishtpy  22771  isphtpy  22780  om1elbas  22832  iscfil  23063  iscau  23074  iscmet  23082  lmle  23099  rrxfsupp  23185  minveclem3  23200  minveclem4  23203  ovolshftlem1  23277  ovolscalem1  23281  ovolicc2lem3  23287  iundisj  23316  dyadmax  23366  dyadmbllem  23367  opnmbllem  23369  vitalilem2  23378  vitalilem3  23379  elcpn  23697  ig1pval3  23934  coelem  23982  quotlem  24055  elqaalem1  24074  elqaalem3  24076  aannenlem1  24083  aannenlem2  24084  aalioulem2  24088  radcnv0  24170  dmarea  24684  jensen  24715  ftalem4  24802  ftalem5  24803  efnnfsumcl  24829  efchtdvds  24885  sqff1o  24908  fsumdvdsdiaglem  24909  dvdsppwf1o  24912  dvdsflf1o  24913  dvdsflsumcom  24914  musum  24917  muinv  24919  logfac2  24942  dchrelbas  24961  dchrfi  24980  lgsfle1  25031  lgsle1  25037  lgsdirprm  25056  lgsne0  25060  lgsquadlem1  25105  lgsquadlem2  25106  2lgslem1b  25117  dchrvmasumlem1  25184  logsqvma  25231  pntleml  25300  tgellng  25448  mircgr  25552  mirbtwn  25553  iseqlg  25747  ttgelitv  25763  upgrle  25985  upgrbi  25988  umgredg2  25995  umgrbi  25996  upgr1elem  26007  edgupgr  26029  edgumgr  26030  upgredg  26032  numedglnl  26039  edgusgr  26055  usgruspgrb  26076  usgredg2ALT  26085  ushgredgedg  26121  ushgredgedgloop  26123  usgrexmplef  26151  subumgredg2  26177  subupgr  26179  upgrreslem  26196  umgrreslem  26197  upgrres1  26205  nbgrel  26238  nbupgrel  26241  nbumgrvtx  26242  nbusgreledg  26249  nbgrnself  26257  nbusgredgeu0  26270  nbusgrf1o0  26271  uvtxael  26288  uvtxael1  26296  uvtxusgrel  26304  1hevtxdg1  26402  umgr2v2e  26421  vtxdgoddnumeven  26449  rgrusgrprc  26485  rgrx0ndm  26489  lfgrwlkprop  26584  iswwlks  26728  iswwlksn  26730  wwlknon  26742  wspthnon  26743  wwlksn0  26748  wlknwwlksnsur  26776  wlkwwlksur  26783  wwlksnextsur  26795  wlksnwwlknvbij  26803  wwlks2onv  26847  rusgrnumwwlkslem  26864  rusgrnumwwlks  26869  isclwwlks  26880  isclwwlksn  26882  clwwlksvbij  26922  clwwlksnscsh  26940  eleclclwwlksn  26953  clwwlksnun  26974  eupth2lems  27098  konigsberglem4  27117  fusgreg2wsplem  27197  numclwwlkovfel2  27216  numclwwlkovgel  27221  numclwlk1lem2foa  27224  numclwlk1lem2f  27225  numclwwlk2lem1  27235  numclwlk2lem2f  27236  numclwlk2lem2f1o  27238  grpoidinv2  27369  grpoinv  27379  isssp  27579  islno  27608  isblo  27637  ishmo  27666  ubthlem1  27726  ubthlem2  27727  htthlem  27774  ocel  28140  shsval2i  28246  ococin  28267  chsupsn  28272  eleigvec  28816  cnlnadjlem5  28930  shatomistici  29220  hatomistici  29221  nnindf  29565  ordtconnlem1  29970  indf1ofs  30088  sigagenval  30203  ldsysgenld  30223  ldgenpisyslem1  30226  ldgenpisyslem2  30227  ldgenpisys  30229  ddemeas  30299  ismbfm  30314  imambfm  30324  dya2iocuni  30345  oms0  30359  omssubadd  30362  elcarsg  30367  issibf  30395  sitgfval  30403  oddpwdc  30416  eulerpartlemgh  30440  eulerpartlemgs2  30442  dstfrvel  30535  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemiex  30563  ballotlemfrcn0  30591  ballotlemirc  30593  ballotlem7  30597  reprsum  30691  reprsuc  30693  reprpmtf1o  30704  reprdifc  30705  connpconn  31217  iscvm  31241  cvmsi  31247  cvmsval  31248  cvmliftmolem2  31264  cvmliftiota  31283  snmlval  31313  elmpst  31433  sltval2  31809  sltres  31815  conway  31910  scutcut  31912  scutbday  31913  scutun12  31917  scutbdaybnd  31921  scutbdaylt  31922  lineelsb2  32255  linerflx1  32256  fwddifval  32269  fwddifnval  32270  rankeq1o  32278  finminlem  32312  fneint  32343  fnessref  32352  topmeet  32359  topjoin  32360  neifg  32366  relowlssretop  33211  fin2solem  33395  fin2so  33396  poimirlem4  33413  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  poimirlem31  33440  poimirlem32  33441  opnmbllem0  33445  mblfinlem2  33447  itg2gt0cn  33465  indexa  33528  nninfnub  33547  istotbnd  33568  sstotbnd2  33573  isbnd  33579  isrngohom  33764  isrngoiso  33777  isidl  33813  ispridl  33833  ismaxidl  33839  prnc  33866  isfldidl  33867  islshp  34266  lssats  34299  islfl  34347  isat  34573  atlatmstc  34606  islln  34792  islpln  34816  islvol  34859  linepsubN  35038  elpmap  35044  pmapsub  35054  elpadd  35085  paddvaln0N  35087  islhp  35282  isldil  35396  isltrn  35405  isdilN  35441  istrnN  35444  diaval  36321  diaelval  36322  diaeldm  36325  diaelrnN  36334  cdlemm10N  36407  docaclN  36413  dibglbN  36455  dicval  36465  dicfnN  36472  dicvalrelN  36474  dihglblem2aN  36582  dihglblem2N  36583  dihglblem3N  36584  dih1dimatlem  36618  dihglb2  36631  dochvalr  36646  doch2val2  36653  dochocss  36655  islpolN  36772  mapd0  36954  isnacs  37267  elmzpcl  37289  mzpindd  37309  rencldnfilem  37384  irrapxlem6  37391  pellexlem3  37395  pellexlem5  37397  elpell1qr  37411  elpell14qr  37413  elpell1234qr  37415  pellfundre  37445  pellfundge  37446  pellfundlb  37448  pellfundglb  37449  rmspecnonsq  37472  jm2.22  37562  jm2.23  37563  rpnnen3lem  37598  fnwe2lem2  37621  fnwe2lem3  37622  elmnc  37706  dgraalem  37715  dgraaub  37718  mpaalem  37722  rgspnmin  37741  issdrg  37767  rfovcnvf1od  38298  nzss  38516  iccshift  39744  iooshift  39748  limcperiod  39860  sumnnodd  39862  ioodvbdlimc1lem1  40146  dvnprodlem1  40161  dvnprodlem3  40163  itgperiod  40197  stoweidlem14  40231  stoweidlem15  40232  stoweidlem16  40233  stoweidlem31  40248  stoweidlem36  40253  stoweidlem46  40263  stoweidlem48  40265  fourierdlem2  40326  fourierdlem3  40327  fourierdlem20  40344  fourierdlem25  40349  fourierdlem37  40361  fourierdlem42  40366  fourierdlem48  40371  fourierdlem51  40374  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem79  40402  fourierdlem81  40404  elaa2lem  40450  etransclem24  40475  etransclem26  40477  etransclem28  40479  etransclem35  40486  etransclem48  40499  salgenval  40541  salgenn0  40549  salgencl  40550  sssalgen  40553  salgenss  40554  salgenuni  40555  issalgend  40556  salgencntex  40561  subsaliuncllem  40575  sge0fodjrnlem  40633  meadjiunlem  40682  caragenel  40709  ovnlecvr  40772  ovnpnfelsup  40773  ovncvrrp  40778  ovnsubaddlem1  40784  hoidmv1lelem1  40805  hoidmv1lelem2  40806  hoidmv1lelem3  40807  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem4  40812  ovnhoilem1  40815  ovnlecvr2  40824  ovncvr2  40825  issmflem  40936  smflimlem2  40980  smflimlem3  40981  smflimsuplem2  41027  iccpart  41352  dfodd2  41549  dfeven5  41578  dfodd7  41579  1hegrlfgr  41713  sprel  41734  prelspr  41736  sprsymrelfolem2  41743  sprsymrelf  41745  ismgmhm  41783  issubmgm  41789  rabsubmgmd  41791  mgmhmeql  41803  assintop  41845  isassintop  41846  assintopcllaw  41848  isrnghm  41892  isrngisom  41896  0even  41931  2even  41933  2zrngamgm  41939  dmatALTbasel  42191  lcoval  42201  elbigo  42345  secval  42488  cscval  42489  cotval  42490