Metamath Proof Explorer


Theorem elab2gw

Description: Membership in a class abstraction, using two substitution hypotheses to avoid a disjoint variable condition on x and A , which is not usually significant since B is usually a constant. (Contributed by SN, 16-May-2024)

Ref Expression
Hypotheses elabgw.1 x=yφψ
elabgw.2 y=Aψχ
elab2gw.3 B=x|φ
Assertion elab2gw AVABχ

Proof

Step Hyp Ref Expression
1 elabgw.1 x=yφψ
2 elabgw.2 y=Aψχ
3 elab2gw.3 B=x|φ
4 3 eleq2i ABAx|φ
5 1 2 elabgw AVAx|φχ
6 4 5 syl5bb AVABχ