Theorem elrab2 1954

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 1585	. 2 |- (A e. C <-> A e. {x e. B | ph})
3		elrab2.1	. . 3 |- (x = A -> (ph <-> ps))
4	3	elrab 1952	. 2 |- (A e. {x e. B | ph} <-> (A e. B /\ ps))
5	2, 4	bitri 180	1 |- (A e. C <-> (A e. B /\ ps))

Syntax hints:   -> wi 3   <-> wb 153   /\ wa 230   = wceq 997   e. wcel 999  {crab 1695

This theorem is referenced by:  oawordeulem 4246  inf3lema 4671  zorn2lem2 4851  elrp 6107  elz 6219  uzwo3lem2 6302  repos 6425  sqrlem4 6766  seq1ubi 7002  caucvglem1 7247  ivthlem4 7374  ivthlem6 7376  ivthlem7 7377  ivthlem9 7379  infpn2 7601  ishaus 7868  iscms 8031  isabl 8185  isbn 8608  pilem1 8754  pilem2 8755  pilem3 8756  efif 8804  efifo 8812  efielcirc 8822  circgrp 8823  eff1i 8827  effoi 8828  projlem8 9276  projlem10 9278  projlem13 9281  projlem15 9283  elbdop 9870  hmopidmchi 10162  hmopidmpji 10163  ela 10350  ist1 10693  iscon 10701  iscon2 10702

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-12 1009  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022  df-sb 1214  df-clab 1510  df-cleq 1515  df-clel 1518  df-rab 1699  df-v 1859

Copyright terms: Public domain