Theorem wl-cbvalnae

Description: A more general version of cbval when nonfree properties depend on a distinctor. Such expressions arise in proofs aiming at the elimination of distinct variable constraints, specifically in application of dvelimf , nfsb2 or dveeq1 . (Contributed by Wolf Lammen, 4-Jun-2019)

	Ref	Expression
Hypotheses	wl-cbvalnae.1	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝜑 )
	wl-cbvalnae.2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝜓 )
	wl-cbvalnae.3	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	wl-cbvalnae	⊢ ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		wl-cbvalnae.1	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝜑 )
2		wl-cbvalnae.2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝜓 )
3		wl-cbvalnae.3	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
4		nftru	⊢ Ⅎ 𝑥 ⊤
5		nftru	⊢ Ⅎ 𝑦 ⊤
6	1	a1i	⊢ ( ⊤ → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝜑 ) )
7	2	a1i	⊢ ( ⊤ → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝜓 ) )
8	3	a1i	⊢ ( ⊤ → ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) )
9	4 5 6 7 8	wl-cbvalnaed	⊢ ( ⊤ → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 𝜓 ) )
10	9	mptru	⊢ ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 𝜓 )