Theorem elrab2 1898

Description: Membership in a class abstraction, using implicit substitution.

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

Proof of Theorem elrab2

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

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 953   e. wcel 955  {crab 1640

This theorem is referenced by:  oawordeulem 4172  inf3lema 4581  zorn2lem2 4761  elz 6084  uzwo3lem2 6165  elrp 6220  repos 6332  sqrlem4 6606  seq1ub 6849  caucvglem1 7093  ivthlem4 7219  ivthlem6 7221  ivthlem7 7222  ivthlem9 7224  ivthlem4OLD 7228  ivthlem6OLD 7230  ivthlem7OLD 7231  infpn2 7452  ishaus 7722  iscms 7881  isabl 8037  isbn 8455  pilem1 8590  pilem2 8591  pilem3 8592  efif 8636  efifo 8644  elcircOLD 8654  efielcirc 8659  circgrp 8660  eff1i 8665  effoi 8666  effoiOLD 8667  projlem8 9109  projlem10 9111  projlem13 9114  projlem15 9116  elbdopt 9704  hmopidmch 9990  hmopidmpj 9991  elat 10174  ist1 10458

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-rab 1644  df-v 1803

Copyright terms: Public domain