Metamath Proof Explorer


Theorem rabeqel

Description: Class element of a restricted class abstraction. (Contributed by Peter Mazsa, 24-Jul-2021)

Ref Expression
Hypotheses rabeqel.1
|- B = { x e. A | ph }
rabeqel.2
|- ( x = C -> ( ph <-> ps ) )
Assertion rabeqel
|- ( C e. B <-> ( ps /\ C e. A ) )

Proof

Step Hyp Ref Expression
1 rabeqel.1
 |-  B = { x e. A | ph }
2 rabeqel.2
 |-  ( x = C -> ( ph <-> ps ) )
3 2 1 elrab2
 |-  ( C e. B <-> ( C e. A /\ ps ) )
4 3 biancomi
 |-  ( C e. B <-> ( ps /\ C e. A ) )