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

Metamath Proof Explorer

Theorem bj-nnflemee

Description: One of four lemmas for nonfreeness: antecedent and consequent both expressed using existential quantifier. (Contributed by BJ, 12-Aug-2023) (Proof modification is discouraged.)

Ref Expression
Assertion bj-nnflemee ⊢ ∀ x ∃ y φ → φ → ∃ y ∃ x φ → ∃ x φ

Proof

Step Hyp Ref Expression
1 excom ⊢ ∃ y ∃ x φ ↔ ∃ x ∃ y φ
2 exim ⊢ ∀ x ∃ y φ → φ → ∃ x ∃ y φ → ∃ x φ
3 1 2 biimtrid ⊢ ∀ x ∃ y φ → φ → ∃ y ∃ x φ → ∃ x φ