Theorem hbexg

Description: Closed form of nfex . Derived from hbexgVD . (Contributed by Alan Sare, 8-Feb-2014) (Revised by Mario Carneiro, 12-Dec-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	hbexg	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 ) → ∀ 𝑥 ∀ 𝑦 ( ∃ 𝑦 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		nfa2	⊢ Ⅎ 𝑦 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 )
2		sp	⊢ ( ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 ) → ( 𝜑 → ∀ 𝑥 𝜑 ) )
3	2	alimi	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 ) → ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) )
4		nf5	⊢ ( Ⅎ 𝑥 𝜑 ↔ ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) )
5	3 4	sylibr	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 ) → Ⅎ 𝑥 𝜑 )
6	1 5	nfexd	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 ) → Ⅎ 𝑥 ∃ 𝑦 𝜑 )
7		nf5	⊢ ( Ⅎ 𝑥 ∃ 𝑦 𝜑 ↔ ∀ 𝑥 ( ∃ 𝑦 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜑 ) )
8	6 7	sylib	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 ) → ∀ 𝑥 ( ∃ 𝑦 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜑 ) )
9	1 8	alrimi	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 ) → ∀ 𝑦 ∀ 𝑥 ( ∃ 𝑦 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜑 ) )
10		alcom	⊢ ( ∀ 𝑦 ∀ 𝑥 ( ∃ 𝑦 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ∃ 𝑦 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜑 ) )
11	9 10	sylib	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 ) → ∀ 𝑥 ∀ 𝑦 ( ∃ 𝑦 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜑 ) )