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		df-sb	|- ( [ 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		df-sb	|- ( [ 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 )