Theorem wl-sb9v

Description: Commutation of quantification and substitution variables based on fewer axioms than sb9 . (Contributed by Wolf Lammen, 27-Apr-2025)

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

Proof

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