Theorem 19.12vv

Description: Special case of 19.12 where its converse holds. See 19.12vvv for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 18-Jul-2001) (Revised by Andrew Salmon, 11-Jul-2011)

	Ref	Expression
Assertion	19.12vv	⊢ ( ∃ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) ↔ ∀ 𝑦 ∃ 𝑥 ( 𝜑 → 𝜓 ) )

Proof

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