Theorem elrab2 2985

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 2-Nov-2006.)

Hypotheses

Ref	Expression
elrab2.1	|- ( x = A -> ( ph <-> ps ) )
elrab2.2	|- C = { x e. B | ph }

Assertion

Ref	Expression
elrab2	|- ( A e. C <-> ( A e. B /\ ps ) )

Distinct variable groups:   ps, x   x, A   x, B

Allowed substitution hints:   ph( x)   C( x)

Proof of Theorem elrab2

Step	Hyp	Ref	Expression
1		elrab2.2	. . 3 |- C = { x e. B | ph }
2	1	eleq2i 2305	. 2 |- ( A e. C <-> A e. { x e. B | ph } )
3		elrab2.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
4	3	elrab 2982	. 2 |- ( A e. { x e. B | ph } <-> ( A e. B /\ ps ) )
5	2, 4	bitri 184	1 |- ( A e. C <-> ( A e. B /\ ps ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1402   e. wcel 2209   {crab 2532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rab 2537  df-v 2823

This theorem is used by:  elrabsf  3090  pwnss  4298  regexmidlemm  4681  regexmidlem1  4682  reg2exmidlema  4683  tfis  4732  ctssdccl  7457  nninff  7468  nninfninc  7469  infnninf  7470  infnninfOLD  7471  nnnninf  7472  nnnninfeq  7474  nnnninfeq2  7475  nninfwlpoimlemg  7521  exmidaclem  7570  ltexprlemell  7971  ltexprlemelu  7972  cauappcvgprlemm  8018  cauappcvgprlemopl  8019  cauappcvgprlemlol  8020  cauappcvgprlemopu  8021  cauappcvgprlemupu  8022  cauappcvgprlemdisj  8024  cauappcvgprlemloc  8025  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  cauappcvgprlem2  8033  caucvgprlemm  8041  caucvgprlemopl  8042  caucvgprlemlol  8043  caucvgprlemopu  8044  caucvgprlemupu  8045  caucvgprlemdisj  8047  caucvgprlemloc  8048  caucvgprlemladdfu  8050  caucvgprlem2  8053  caucvgprprlemell  8058  caucvgprprlemelu  8059  caucvgprprlemml  8067  caucvgprprlemmu  8068  caucvgprprlemexbt  8079  caucvgprprlem2  8083  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  axpre-suploclemres  8274  elz  9657  elrp  10073  repos  10389  zsupssdc  10690  bitsfzolem  12746  isprm  12912  nnmaxpw  12978  sqpweven  12980  2sqpwodd  12981  phimullem  13032  eulerthlem1  13034  eulerthlemfi  13035  eulerthlemrprm  13036  eulerthlemth  13039  hashgcdlem  13045  pclem0  13094  pclemub  13095  pclemdc  13096  pcprecl  13097  pcprendvds  13098  1arith  13175  elgz  13179  4sqlem13m  13211  4sqlem17  13215  4sqlem18  13216  ballotfilemelo  13280  ballotfileme  13294  ballotfilemscl  13305  ctiunctlemu1st  13383  ctiunctlemu2nd  13384  ctiunctlemudc  13386  ctiunctlemfo  13388  infpn2  13405  issgrp  13777  ismnddef  13790  gsumvallem2  13859  isgrp  13870  elnmz  14070  iscmn  14186  isrng  14340  issrg  14376  isring  14411  iscrng  14414  isnzr  14597  islring  14608  isrrg  14680  isdomn  14687  isdrngtap  14715  islmod  14736  isassa  15111  psrbag  15162  psrbagconcl  15173  gsumbagdiaglem  15175  psr1clfi  15198  isxms  15677  isms  15679  ivthinclemlm  15860  ivthinclemum  15861  ivthinclemlopn  15862  ivthinclemlr  15863  ivthinclemuopn  15864  ivthinclemur  15865  ivthinclemdisj  15866  ivthinclemloc  15867  zprmlogbaplem3  16217  mpodvdsmulf1o  16284  lgslem2  16325  lgslem3  16326  lgsfcl2  16330  lfgredg2dom  16578  uspgredg2vlem  16666  uspgredg2v  16667  usgredg2vlem1  16668  usgredg2vlem2  16669  ushgredgedg  16672  ushgredgedgloop  16674  isclwwlknon  16876  s2elclwwlknon2  16882  0nninf  17253  nnsf  17254  peano4nninf  17255  nninfalllem1  17257  nninfself  17262  qdencn  17278