Metamath Proof Explorer


Theorem ac6sf2

Description: Alternate version of ac6 with bound-variable hypothesis. (Contributed by NM, 2-Mar-2008) (Revised by Thierry Arnoux, 17-May-2020)

Ref Expression
Hypotheses ac6sf2.y _ y B
ac6sf2.1 y ψ
ac6sf2.2 A V
ac6sf2.3 y = f x φ ψ
Assertion ac6sf2 x A y B φ f f : A B x A ψ

Proof

Step Hyp Ref Expression
1 ac6sf2.y _ y B
2 ac6sf2.1 y ψ
3 ac6sf2.2 A V
4 ac6sf2.3 y = f x φ ψ
5 nfcv _ z B
6 nfv z φ
7 nfs1v y z y φ
8 sbequ12 y = z φ z y φ
9 1 5 6 7 8 cbvrexfw y B φ z B z y φ
10 9 ralbii x A y B φ x A z B z y φ
11 2 4 sbhypf z = f x z y φ ψ
12 3 11 ac6s x A z B z y φ f f : A B x A ψ
13 10 12 sylbi x A y B φ f f : A B x A ψ