Theorem cbvalvOLD

Description: Obsolete version of cbvalv as of 11-Sep-2023. (Contributed by NM, 5-Aug-1993) Remove dependency on ax-10 . (Revised by Wolf Lammen, 17-Jul-2021) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	cbvalv.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	cbvalvOLD	⊢ ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		cbvalv.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		ax-5	⊢ ( 𝜑 → ∀ 𝑦 𝜑 )
3	2	hbal	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 )
4	1	spv	⊢ ( ∀ 𝑥 𝜑 → 𝜓 )
5	3 4	alrimih	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 )
6		ax-5	⊢ ( 𝜓 → ∀ 𝑥 𝜓 )
7	6	hbal	⊢ ( ∀ 𝑦 𝜓 → ∀ 𝑥 ∀ 𝑦 𝜓 )
8	1	equcoms	⊢ ( 𝑦 = 𝑥 → ( 𝜑 ↔ 𝜓 ) )
9	8	bicomd	⊢ ( 𝑦 = 𝑥 → ( 𝜓 ↔ 𝜑 ) )
10	9	spv	⊢ ( ∀ 𝑦 𝜓 → 𝜑 )
11	7 10	alrimih	⊢ ( ∀ 𝑦 𝜓 → ∀ 𝑥 𝜑 )
12	5 11	impbii	⊢ ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 𝜓 )