Theorem bj-exextruan

Description: An equivalent expression for existential quantification over a non-occurring variable proved over ax-1 -- ax-5 . The forward implication can be seen as a strengthening of ax-5 (a conjunct is added to the consequent of the implication). The reverse implication can be strengthened when ax-6 is posited (which implies that models are non-empty), see 19.8v . See bj-alextruim for a dual statement.

An approximate meaning is: the existential quantification of a proposition over a non-occurring variable holds if and only if the proposition holds and the universe is nonempty. (Contributed by BJ, 14-Mar-2026) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-exextruan	⊢ ( ∃ 𝑥 𝜑 ↔ ( ∃ 𝑥 ⊤ ∧ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		trud	⊢ ( 𝜑 → ⊤ )
2	1	eximi	⊢ ( ∃ 𝑥 𝜑 → ∃ 𝑥 ⊤ )
3		ax5e	⊢ ( ∃ 𝑥 𝜑 → 𝜑 )
4	2 3	jca	⊢ ( ∃ 𝑥 𝜑 → ( ∃ 𝑥 ⊤ ∧ 𝜑 ) )
5		bj-spvew	⊢ ( ∃ 𝑥 ⊤ → ( 𝜑 ↔ ∃ 𝑥 𝜑 ) )
6	5	biimpa	⊢ ( ( ∃ 𝑥 ⊤ ∧ 𝜑 ) → ∃ 𝑥 𝜑 )
7	4 6	impbii	⊢ ( ∃ 𝑥 𝜑 ↔ ( ∃ 𝑥 ⊤ ∧ 𝜑 ) )