This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 ) → ∀ 𝑥 ∀ 𝑦 ( ∃ 𝑦 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜑 ) )