Metamath Proof Explorer

Theorem elab2gw

Description: Membership in a class abstraction, using implicit substitution and an intermediate setvar y to avoid ax-10 , ax-11 , ax-12 . It also avoids a disjoint variable condition on x and A . (Contributed by SN, 16-May-2024)

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


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