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	$$⊢\exists x\phi \leftrightarrow \left(\exists x\top \wedge \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		trud	$$⊢\phi \to \top$$
2	1	eximi	$$⊢\exists x\phi \to \exists x\top$$
3		ax5e	$$⊢\exists x\phi \to \phi$$
4	2 3	jca	$$⊢\exists x\phi \to \left(\exists x\top \wedge \phi \right)$$
5		bj-spvew	$$⊢\exists x\top \to \left(\phi \leftrightarrow \exists x\phi \right)$$
6	5	biimpa	$$⊢\left(\exists x\top \wedge \phi \right)\to \exists x\phi$$
7	4 6	impbii	$$⊢\exists x\phi \leftrightarrow \left(\exists x\top \wedge \phi \right)$$