Theorem sb8v

Description: Substitution of variable in universal quantifier. Version of sb8f with a disjoint variable condition replacing the nonfree hypothesis F/ y ph , not requiring ax-12 . (Contributed by SN, 5-Dec-2024)

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

Proof

Step	Hyp	Ref	Expression
1		sb6	|- ( [ y / x ] ph <-> A. x ( x = y -> ph ) )
2	1	albii	|- ( A. y [ y / x ] ph <-> A. y A. x ( x = y -> ph ) )
3		alcom	|- ( A. y A. x ( x = y -> ph ) <-> A. x A. y ( x = y -> ph ) )
4		equcom	|- ( x = y <-> y = x )
5	4	imbi1i	|- ( ( x = y -> ph ) <-> ( y = x -> ph ) )
6	5	albii	|- ( A. y ( x = y -> ph ) <-> A. y ( y = x -> ph ) )
7		equsv	|- ( A. y ( y = x -> ph ) <-> ph )
8	6 7	bitri	|- ( A. y ( x = y -> ph ) <-> ph )
9	8	albii	|- ( A. x A. y ( x = y -> ph ) <-> A. x ph )
10	2 3 9	3bitrri	|- ( A. x ph <-> A. y [ y / x ] ph )