Metamath Proof Explorer


Theorem bj-eximALT

Description: Alternate proof of exim directly from alim by using df-ex (using duality of A. and E. . (Contributed by BJ, 9-Dec-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion bj-eximALT ( ∀ 𝑥 ( 𝜑𝜓 ) → ( ∃ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) )

Proof

Step Hyp Ref Expression
1 con3 ( ( 𝜑𝜓 ) → ( ¬ 𝜓 → ¬ 𝜑 ) )
2 1 alimi ( ∀ 𝑥 ( 𝜑𝜓 ) → ∀ 𝑥 ( ¬ 𝜓 → ¬ 𝜑 ) )
3 alim ( ∀ 𝑥 ( ¬ 𝜓 → ¬ 𝜑 ) → ( ∀ 𝑥 ¬ 𝜓 → ∀ 𝑥 ¬ 𝜑 ) )
4 con3 ( ( ∀ 𝑥 ¬ 𝜓 → ∀ 𝑥 ¬ 𝜑 ) → ( ¬ ∀ 𝑥 ¬ 𝜑 → ¬ ∀ 𝑥 ¬ 𝜓 ) )
5 2 3 4 3syl ( ∀ 𝑥 ( 𝜑𝜓 ) → ( ¬ ∀ 𝑥 ¬ 𝜑 → ¬ ∀ 𝑥 ¬ 𝜓 ) )
6 df-ex ( ∃ 𝑥 𝜑 ↔ ¬ ∀ 𝑥 ¬ 𝜑 )
7 df-ex ( ∃ 𝑥 𝜓 ↔ ¬ ∀ 𝑥 ¬ 𝜓 )
8 5 6 7 3imtr4g ( ∀ 𝑥 ( 𝜑𝜓 ) → ( ∃ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) )