Metamath Proof Explorer


Theorem sbcexf

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

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

Proof

Step Hyp Ref Expression
1 sbcexf.1 _ y A
2 nfv z φ
3 2 sb8ev y φ z z y φ
4 3 sbcbii [˙A / x]˙ y φ [˙A / x]˙ z z y φ
5 sbcex2 [˙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 cbvexv1 z [˙A / x]˙ z y φ y [˙A / x]˙ φ
12 4 5 11 3bitri [˙A / x]˙ y φ y [˙A / x]˙ φ