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

Metamath Proof Explorer

Theorem moabexOLD

Description: Obsolete version of moabex as of 2-Feb-2026. (Contributed by NM, 30-Dec-1996) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	moabexOLD	⊢ ( ∃* 𝑥 𝜑 → { 𝑥 ∣ 𝜑 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		df-mo	⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
2		abss	⊢ ( { 𝑥 ∣ 𝜑 } ⊆ { 𝑦 } ↔ ∀ 𝑥 ( 𝜑 → 𝑥 ∈ { 𝑦 } ) )
3		velsn	⊢ ( 𝑥 ∈ { 𝑦 } ↔ 𝑥 = 𝑦 )
4	3	imbi2i	⊢ ( ( 𝜑 → 𝑥 ∈ { 𝑦 } ) ↔ ( 𝜑 → 𝑥 = 𝑦 ) )
5	4	albii	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 ∈ { 𝑦 } ) ↔ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
6	2 5	bitri	⊢ ( { 𝑥 ∣ 𝜑 } ⊆ { 𝑦 } ↔ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
7		vsnex	⊢ { 𝑦 } ∈ V
8	7	ssex	⊢ ( { 𝑥 ∣ 𝜑 } ⊆ { 𝑦 } → { 𝑥 ∣ 𝜑 } ∈ V )
9	6 8	sylbir	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → { 𝑥 ∣ 𝜑 } ∈ V )
10	9	exlimiv	⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → { 𝑥 ∣ 𝜑 } ∈ V )
11	1 10	sylbi	⊢ ( ∃* 𝑥 𝜑 → { 𝑥 ∣ 𝜑 } ∈ V )