Metamath Proof Explorer


Theorem sbcalf

Description: Move universal quantifier in and out of class substitution, with an explicit nonfree variable condition. (Contributed by Giovanni Mascellani, 29-May-2019)

Ref Expression
Hypothesis sbcalf.1 _ y A
Assertion sbcalf [˙A / x]˙ y φ y [˙A / x]˙ φ

Proof

Step Hyp Ref Expression
1 sbcalf.1 _ y A
2 nfv z φ
3 2 sb8v y φ z z y φ
4 3 sbcbii [˙A / x]˙ y φ [˙A / x]˙ z z y φ
5 sbcal [˙A / x]˙ z z y φ z [˙A / x]˙ z y φ
6 nfs1v y z y φ
7 1 6 nfsbcw y [˙A / x]˙ z y φ
8 nfv z [˙A / x]˙ φ
9 sbequ12r z = y z y φ φ
10 9 sbcbidv z = y [˙A / x]˙ z y φ [˙A / x]˙ φ
11 7 8 10 cbvalv1 z [˙A / x]˙ z y φ y [˙A / x]˙ φ
12 4 5 11 3bitri [˙A / x]˙ y φ y [˙A / x]˙ φ