Theorem 19.12b

Description: Version of 19.12vv with not-free hypotheses, instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010) (Revised by Mario Carneiro, 11-Dec-2016)

	Ref	Expression
Hypotheses	19.12b.1	⊢ Ⅎ 𝑦 𝜑
	19.12b.2	⊢ Ⅎ 𝑥 𝜓
Assertion	19.12b	⊢ ( ∃ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) ↔ ∀ 𝑦 ∃ 𝑥 ( 𝜑 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		19.12b.1	⊢ Ⅎ 𝑦 𝜑
2		19.12b.2	⊢ Ⅎ 𝑥 𝜓
3	1	19.21	⊢ ( ∀ 𝑦 ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → ∀ 𝑦 𝜓 ) )
4	3	exbii	⊢ ( ∃ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) ↔ ∃ 𝑥 ( 𝜑 → ∀ 𝑦 𝜓 ) )
5	2	nfal	⊢ Ⅎ 𝑥 ∀ 𝑦 𝜓
6	5	19.36	⊢ ( ∃ 𝑥 ( 𝜑 → ∀ 𝑦 𝜓 ) ↔ ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) )
7	2	19.36	⊢ ( ∃ 𝑥 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 𝜑 → 𝜓 ) )
8	7	albii	⊢ ( ∀ 𝑦 ∃ 𝑥 ( 𝜑 → 𝜓 ) ↔ ∀ 𝑦 ( ∀ 𝑥 𝜑 → 𝜓 ) )
9	1	nfal	⊢ Ⅎ 𝑦 ∀ 𝑥 𝜑
10	9	19.21	⊢ ( ∀ 𝑦 ( ∀ 𝑥 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) )
11	8 10	bitr2i	⊢ ( ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) ↔ ∀ 𝑦 ∃ 𝑥 ( 𝜑 → 𝜓 ) )
12	4 6 11	3bitri	⊢ ( ∃ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) ↔ ∀ 𝑦 ∃ 𝑥 ( 𝜑 → 𝜓 ) )