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 𝑦 𝐴
Assertion sbcalf ( [ 𝐴 / 𝑥 ]𝑦 𝜑 ↔ ∀ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 )

Proof

Step Hyp Ref Expression
1 sbcalf.1 𝑦 𝐴
2 nfv 𝑧 𝜑
3 2 sb8v ( ∀ 𝑦 𝜑 ↔ ∀ 𝑧 [ 𝑧 / 𝑦 ] 𝜑 )
4 3 sbcbii ( [ 𝐴 / 𝑥 ]𝑦 𝜑[ 𝐴 / 𝑥 ]𝑧 [ 𝑧 / 𝑦 ] 𝜑 )
5 sbcal ( [ 𝐴 / 𝑥 ]𝑧 [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑧 [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 )
6 nfs1v 𝑦 [ 𝑧 / 𝑦 ] 𝜑
7 1 6 nfsbcw 𝑦 [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑
8 nfv 𝑧 [ 𝐴 / 𝑥 ] 𝜑
9 sbequ12r ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑦 ] 𝜑𝜑 ) )
10 9 sbcbidv ( 𝑧 = 𝑦 → ( [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑[ 𝐴 / 𝑥 ] 𝜑 ) )
11 7 8 10 cbvalv1 ( ∀ 𝑧 [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 )
12 4 5 11 3bitri ( [ 𝐴 / 𝑥 ]𝑦 𝜑 ↔ ∀ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 )