This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbal

Description: Move universal quantifier in and out of substitution. (Contributed by NM, 16-May-1993) (Proof shortened by Wolf Lammen, 29-Sep-2018) Reduce dependencies on axioms. (Revised by Steven Nguyen, 13-Aug-2023)

Ref Expression
Assertion sbal 
|- ( [ z / y ] A. x ph <-> A. x [ z / y ] ph )

Proof

Step Hyp Ref Expression
1 alcom 
 |-  ( A. w A. x ( w = z -> A. y ( y = w -> ph ) ) <-> A. x A. w ( w = z -> A. y ( y = w -> ph ) ) )
2 19.21v 
 |-  ( A. x ( y = w -> ph ) <-> ( y = w -> A. x ph ) )
3 2 albii 
 |-  ( A. y A. x ( y = w -> ph ) <-> A. y ( y = w -> A. x ph ) )
4 alcom 
 |-  ( A. y A. x ( y = w -> ph ) <-> A. x A. y ( y = w -> ph ) )
5 3 4 bitr3i 
 |-  ( A. y ( y = w -> A. x ph ) <-> A. x A. y ( y = w -> ph ) )
6 5 imbi2i 
 |-  ( ( w = z -> A. y ( y = w -> A. x ph ) ) <-> ( w = z -> A. x A. y ( y = w -> ph ) ) )
7 6 albii 
 |-  ( A. w ( w = z -> A. y ( y = w -> A. x ph ) ) <-> A. w ( w = z -> A. x A. y ( y = w -> ph ) ) )
8 dfsb 
 |-  ( [ z / y ] A. x ph <-> A. w ( w = z -> A. y ( y = w -> A. x ph ) ) )
9 19.21v 
 |-  ( A. x ( w = z -> A. y ( y = w -> ph ) ) <-> ( w = z -> A. x A. y ( y = w -> ph ) ) )
10 9 albii 
 |-  ( A. w A. x ( w = z -> A. y ( y = w -> ph ) ) <-> A. w ( w = z -> A. x A. y ( y = w -> ph ) ) )
11 7 8 10 3bitr4i 
 |-  ( [ z / y ] A. x ph <-> A. w A. x ( w = z -> A. y ( y = w -> ph ) ) )
12 dfsb 
 |-  ( [ z / y ] ph <-> A. w ( w = z -> A. y ( y = w -> ph ) ) )
13 12 albii 
 |-  ( A. x [ z / y ] ph <-> A. x A. w ( w = z -> A. y ( y = w -> ph ) ) )
14 1 11 13 3bitr4i 
 |-  ( [ z / y ] A. x ph <-> A. x [ z / y ] ph )