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 
|- ( E* x ph -> { x | ph } e. _V )

Proof

Step Hyp Ref Expression
1 df-mo 
 |-  ( E* x ph <-> E. y A. x ( ph -> x = y ) )
2 abss 
 |-  ( { x | ph } C_ { y } <-> A. x ( ph -> x e. { y } ) )
3 velsn 
 |-  ( x e. { y } <-> x = y )
4 3 imbi2i 
 |-  ( ( ph -> x e. { y } ) <-> ( ph -> x = y ) )
5 4 albii 
 |-  ( A. x ( ph -> x e. { y } ) <-> A. x ( ph -> x = y ) )
6 2 5 bitri 
 |-  ( { x | ph } C_ { y } <-> A. x ( ph -> x = y ) )
7 vsnex 
 |-  { y } e. _V
8 7 ssex 
 |-  ( { x | ph } C_ { y } -> { x | ph } e. _V )
9 6 8 sylbir 
 |-  ( A. x ( ph -> x = y ) -> { x | ph } e. _V )
10 9 exlimiv 
 |-  ( E. y A. x ( ph -> x = y ) -> { x | ph } e. _V )
11 1 10 sylbi 
 |-  ( E* x ph -> { x | ph } e. _V )