Metamath Proof Explorer


Theorem elrab2

Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 2-Nov-2006)

Ref Expression
Hypotheses elrab2.1 x = A φ ψ
elrab2.2 C = x B | φ
Assertion elrab2 A C A B ψ

Proof

Step Hyp Ref Expression
1 elrab2.1 x = A φ ψ
2 elrab2.2 C = x B | φ
3 2 eleq2i A C A x B | φ
4 1 elrab A x B | φ A B ψ
5 3 4 bitri A C A B ψ