Metamath Proof Explorer


Theorem ac6sg

Description: ac6s with sethood as antecedent. (Contributed by FL, 3-Aug-2009)

Ref Expression
Hypothesis ac6sg.1 y=fxφψ
Assertion ac6sg AVxAyBφff:ABxAψ

Proof

Step Hyp Ref Expression
1 ac6sg.1 y=fxφψ
2 raleq z=AxzyBφxAyBφ
3 feq2 z=Af:zBf:AB
4 raleq z=AxzψxAψ
5 3 4 anbi12d z=Af:zBxzψf:ABxAψ
6 5 exbidv z=Aff:zBxzψff:ABxAψ
7 2 6 imbi12d z=AxzyBφff:zBxzψxAyBφff:ABxAψ
8 vex zV
9 8 1 ac6s xzyBφff:zBxzψ
10 7 9 vtoclg AVxAyBφff:ABxAψ