Metamath Proof Explorer


Theorem exisym1

Description: A symmetry with E. .

See negsym1 for more information. (Contributed by Anthony Hart, 4-Sep-2011)

Ref Expression
Assertion exisym1 ( ∃ 𝑥𝑥 ⊥ → ∃ 𝑥 𝜑 )

Proof

Step Hyp Ref Expression
1 nfe1 𝑥𝑥 𝜑
2 falim ( ⊥ → 𝜑 )
3 2 eximi ( ∃ 𝑥 ⊥ → ∃ 𝑥 𝜑 )
4 1 3 exlimi ( ∃ 𝑥𝑥 ⊥ → ∃ 𝑥 𝜑 )