Metamath Proof Explorer


Theorem elabgw

Description: Membership in a class abstraction, using two substitution hypotheses to avoid a disjoint variable condition on x and A . This is to elabg what sbievw2 is to sbievw . (Contributed by SN, 20-Apr-2024)

Ref Expression
Hypotheses elabgw.1 x=yφψ
elabgw.2 y=Aψχ
Assertion elabgw AVAx|φχ

Proof

Step Hyp Ref Expression
1 elabgw.1 x=yφψ
2 elabgw.2 y=Aψχ
3 eleq1 y=Ayx|φAx|φ
4 df-clab yx|φyxφ
5 1 sbievw yxφψ
6 4 5 bitri yx|φψ
7 3 2 6 vtoclbg AVAx|φχ