Theorem elrab2 1905

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 1537	. 2 |- (A e. C <-> A e. {x e. B | ph})
3		elrab2.1	. . 3 |- (x = A -> (ph <-> ps))
4	3	elrab 1903	. 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 955   e. wcel 957  {crab 1647

This theorem is referenced by:  oawordeulem 4185  inf3lema 4596  zorn2lem2 4776  elz 6098  uzwo3lem2 6179  elrp 6237  repos 6350  sqrlem4 6627  seq1ub 6878  caucvglem1 7126  ivthlem4 7255  ivthlem6 7257  ivthlem7 7258  ivthlem9 7260  ivthlem4OLD 7264  ivthlem6OLD 7266  ivthlem7OLD 7267  infpn2 7488  ishaus 7762  iscms 7929  isabl 8085  isbn 8508  pilem1 8654  pilem2 8655  pilem3 8656  efif 8700  efifo 8708  elcircOLD 8718  efielcirc 8723  circgrp 8724  eff1i 8728  effoi 8729  projlem8 9181  projlem10 9183  projlem13 9186  projlem15 9188  elbdopt 9778  hmopidmch 10070  hmopidmpj 10071  elat 10257  ist1 10565

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-rab 1651  df-v 1810

Copyright terms: Public domain