Theorem wl-cbvalnaed

Description: wl-cbvalnae with a context. (Contributed by Wolf Lammen, 28-Jul-2019)

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

Proof

Step	Hyp	Ref	Expression
1		wl-cbvalnaed.1	⊢ Ⅎ 𝑥 𝜑
2		wl-cbvalnaed.2	⊢ Ⅎ 𝑦 𝜑
3		wl-cbvalnaed.3	⊢ ( 𝜑 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝜓 ) )
4		wl-cbvalnaed.4	⊢ ( 𝜑 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝜒 ) )
5		wl-cbvalnaed.5	⊢ ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) ) )
6	1 2 5	wl-dral1d	⊢ ( 𝜑 → ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝜓 ↔ ∀ 𝑦 𝜒 ) ) )
7	6	imp	⊢ ( ( 𝜑 ∧ ∀ 𝑥 𝑥 = 𝑦 ) → ( ∀ 𝑥 𝜓 ↔ ∀ 𝑦 𝜒 ) )
8		nfnae	⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦
9	1 8	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 )
10		wl-nfnae1	⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦
11	2 10	nfan	⊢ Ⅎ 𝑦 ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 )
12	3	imp	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑦 𝜓 )
13	4	imp	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝜒 )
14	5	adantr	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) ) )
15	9 11 12 13 14	cbv2	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( ∀ 𝑥 𝜓 ↔ ∀ 𝑦 𝜒 ) )
16	7 15	pm2.61dan	⊢ ( 𝜑 → ( ∀ 𝑥 𝜓 ↔ ∀ 𝑦 𝜒 ) )