Metamath Proof Explorer


Theorem elab2g

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995)

Ref Expression
Hypotheses elab2g.1 x=Aφψ
elab2g.2 B=x|φ
Assertion elab2g AVABψ

Proof

Step Hyp Ref Expression
1 elab2g.1 x=Aφψ
2 elab2g.2 B=x|φ
3 2 eleq2i ABAx|φ
4 1 elabg AVAx|φψ
5 3 4 bitrid AVABψ