Theorem hba1w

Description: Weak version of hba1 . See comments for ax10w . Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017) (Proof shortened by Wolf Lammen, 10-Oct-2021)

	Ref	Expression
Hypothesis	hbn1w.1	|- ( x = y -> ( ph <-> ps ) )
Assertion	hba1w	|- ( A. x ph -> A. x A. x ph )

Proof

Step	Hyp	Ref	Expression
1		hbn1w.1	|- ( x = y -> ( ph <-> ps ) )
2	1	cbvalvw	|- ( A. x ph <-> A. y ps )
3	2	notbii	|- ( -. A. x ph <-> -. A. y ps )
4	3	a1i	|- ( x = y -> ( -. A. x ph <-> -. A. y ps ) )
5	4	spw	|- ( A. x -. A. x ph -> -. A. x ph )
6	5	con2i	|- ( A. x ph -> -. A. x -. A. x ph )
7	4	hbn1w	|- ( -. A. x -. A. x ph -> A. x -. A. x -. A. x ph )
8	1	hbn1w	|- ( -. A. x ph -> A. x -. A. x ph )
9	8	con1i	|- ( -. A. x -. A. x ph -> A. x ph )
10	9	alimi	|- ( A. x -. A. x -. A. x ph -> A. x A. x ph )
11	6 7 10	3syl	|- ( A. x ph -> A. x A. x ph )