Theorem elrab 2894

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 2319	. 2 |- F/_ x A
2		nfcv 2319	. 2 |- F/_ x B
3		nfv 1528	. 2 |- F/ x ps
4		elrab.1	. 2 |- ( x = A -> ( ph <-> ps ) )
5	1, 2, 3, 4	elrabf 2892	1 |- ( A e. { x e. B | ph } <-> ( A e. B /\ ps ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1353   e. wcel 2148   {crab 2459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rab 2464  df-v 2740

This theorem is referenced by:  elrab3  2895  elrabd  2896  elrab2  2897  ralrab  2899  rexrab  2901  rabsnt  3668  unimax  3844  ssintub  3863  intminss  3870  exmidexmid  4197  exmidsssnc  4204  rabxfrd  4470  ordtri2or2exmidlem  4526  onsucelsucexmidlem1  4528  sefvex  5537  ssimaex  5578  acexmidlem2  5872  elpmg  6664  ssfilem  6875  diffitest  6887  inffiexmid  6906  supubti  6998  suplubti  6999  ctssexmid  7148  exmidonfinlem  7192  cc4f  7268  cc4n  7270  caucvgprlemladdfu  7676  caucvgprlemladdrl  7677  suplocexprlemmu  7717  suplocexprlemru  7718  suplocexprlemdisj  7719  suplocexprlemub  7722  nnindnn  7892  negf1o  8339  apsscn  8604  sup3exmid  8914  nnind  8935  peano2uz2  9360  peano5uzti  9361  dfuzi  9363  uzind  9364  uzind3  9366  eluz1  9532  uzind4  9588  supinfneg  9595  infsupneg  9596  eqreznegel  9614  elixx1  9897  elioo2  9921  elfz1  10013  expcl2lemap  10532  expclzaplem  10544  expclzap  10545  expap0i  10552  expge0  10556  expge1  10557  hashennnuni  10759  shftf  10839  reccn2ap  11321  dvdsdivcl  11856  divalgmod  11932  zsupcl  11948  infssuzex  11950  infssuzcldc  11952  bezoutlemsup  12010  dfgcd2  12015  uzwodc  12038  nnwosdc  12040  lcmcllem  12067  lcmledvds  12070  lcmgcdlem  12077  1nprm  12114  1idssfct  12115  isprm2  12117  phicl2  12214  hashdvds  12221  phisum  12240  odzval  12241  odzcllem  12242  odzdvds  12245  oddennn  12393  evenennn  12394  znnen  12399  ennnfonelemg  12404  ennnfonelemom  12409  ismhm  12853  issubm  12863  issubmd  12865  grplinv  12922  issubg  13033  isnsg  13062  issubrg  13342  istopon  13516  epttop  13593  iscld  13606  isnei  13647  neipsm  13657  iscn  13700  iscnp  13702  txdis1cn  13781  ishmeo  13807  ispsmet  13826  ismet  13847  isxmet  13848  elblps  13893  elbl  13894  xmetxpbl  14011  reopnap  14041  divcnap  14058  elcncf  14063  cdivcncfap  14090  cnopnap  14097  ellimc3apf  14132  limccoap  14150  dvlemap  14152  dvidlemap  14163  dvcnp2cntop  14166  dvaddxxbr  14168  dvmulxxbr  14169  dvcoapbr  14174  dvcjbr  14175  dvrecap  14180  dveflem  14190  lgsfle1  14413  lgsle1  14419  lgsdirprm  14438  lgsne0  14442  subctctexmid  14753