# Metamath Proof Explorer

## Theorem sbcalf

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

Ref Expression
Hypothesis sbcalf.1
`|- F/_ y A`
Assertion sbcalf
`|- ( [. A / x ]. A. y ph <-> A. y [. A / x ]. ph )`

### Proof

Step Hyp Ref Expression
1 sbcalf.1
` |-  F/_ y A`
2 nfv
` |-  F/ z ph`
3 2 sb8v
` |-  ( A. y ph <-> A. z [ z / y ] ph )`
4 3 sbcbii
` |-  ( [. A / x ]. A. y ph <-> [. A / x ]. A. z [ z / y ] ph )`
5 sbcal
` |-  ( [. A / x ]. A. z [ z / y ] ph <-> A. z [. A / x ]. [ z / y ] ph )`
6 nfs1v
` |-  F/ y [ z / y ] ph`
7 1 6 nfsbcw
` |-  F/ y [. A / x ]. [ z / y ] ph`
8 nfv
` |-  F/ z [. A / x ]. ph`
9 sbequ12r
` |-  ( z = y -> ( [ z / y ] ph <-> ph ) )`
10 9 sbcbidv
` |-  ( z = y -> ( [. A / x ]. [ z / y ] ph <-> [. A / x ]. ph ) )`
11 7 8 10 cbvalv1
` |-  ( A. z [. A / x ]. [ z / y ] ph <-> A. y [. A / x ]. ph )`
12 4 5 11 3bitri
` |-  ( [. A / x ]. A. y ph <-> A. y [. A / x ]. ph )`