Theorem elrabd 2919

Description: Membership in a restricted class abstraction, using implicit substitution. Deduction version of elrab 2917. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypotheses

Ref	Expression
elrabd.1	|- ( x = A -> ( ps <-> ch ) )
elrabd.2	|- ( ph -> A e. B )
elrabd.3	|- ( ph -> ch )

Assertion

Ref	Expression
elrabd	|- ( ph -> A e. { x e. B | ps } )

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

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

Proof of Theorem elrabd

Step	Hyp	Ref	Expression
1		elrabd.2	. . 3 |- ( ph -> A e. B )
2		elrabd.3	. . 3 |- ( ph -> ch )
3	1, 2	jca 306	. 2 |- ( ph -> ( A e. B /\ ch ) )
4		elrabd.1	. . 3 |- ( x = A -> ( ps <-> ch ) )
5	4	elrab 2917	. 2 |- ( A e. { x e. B | ps } <-> ( A e. B /\ ch ) )
6	3, 5	sylibr 134	1 |- ( ph -> A e. { x e. B | ps } )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1364   e. wcel 2164   {crab 2476

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rab 2481  df-v 2762

This theorem is referenced by:  ctssdccl  7172  suplocexprlemru  7781  suplocexprlemloc  7783  zsupssdc  12094  uzwodc  12177  nninfctlemfo  12180  lcmcllem  12208  lcmledvds  12211  phisum  12381  odzcllem  12383  pcpremul  12434  znnen  12558  ennnfonelemj0  12561  ennnfonelemg  12563  gsumress  12981  issubmd  13049  mhmeql  13067  ghmeql  13340  cdivcncfap  14783  cnopnap  14790  ivthinc  14822  limcdifap  14841  limcimolemlt  14843  dvcoapbr  14886  2lgslem1b  15246  subctctexmid  15561