Metamath Proof Explorer

Theorem rexdif1enOLD

Description: Obsolete version of rexdif1en as of 5-Jan-2025. (Contributed by BTernaryTau, 26-Aug-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion rexdif1enOLD 
|- ( ( M e. _om /\ A ~~ suc M ) -> E. x e. A ( A \ { x } ) ~~ M )

Proof

Step Hyp Ref Expression
1 bren 
 |-  ( A ~~ suc M <-> E. f f : A -1-1-onto-> suc M )
2 19.42v 
 |-  ( E. f ( M e. _om /\ f : A -1-1-onto-> suc M ) <-> ( M e. _om /\ E. f f : A -1-1-onto-> suc M ) )
3 sucidg 
 |-  ( M e. _om -> M e. suc M )
4 f1ocnvdm 
 |-  ( ( f : A -1-1-onto-> suc M /\ M e. suc M ) -> ( `' f ` M ) e. A )
5 4 ancoms 
 |-  ( ( M e. suc M /\ f : A -1-1-onto-> suc M ) -> ( `' f ` M ) e. A )
6 3 5 sylan 
 |-  ( ( M e. _om /\ f : A -1-1-onto-> suc M ) -> ( `' f ` M ) e. A )
7 vex 
 |-  f e. _V
8 dif1enlemOLD 
 |-  ( ( f e. _V /\ M e. _om /\ f : A -1-1-onto-> suc M ) -> ( A \ { ( `' f ` M ) } ) ~~ M )
9 7 8 mp3an1 
 |-  ( ( M e. _om /\ f : A -1-1-onto-> suc M ) -> ( A \ { ( `' f ` M ) } ) ~~ M )
10 sneq 
 |-  ( x = ( `' f ` M ) -> { x } = { ( `' f ` M ) } )
11 10 difeq2d 
 |-  ( x = ( `' f ` M ) -> ( A \ { x } ) = ( A \ { ( `' f ` M ) } ) )
12 11 breq1d 
 |-  ( x = ( `' f ` M ) -> ( ( A \ { x } ) ~~ M <-> ( A \ { ( `' f ` M ) } ) ~~ M ) )
13 12 rspcev 
 |-  ( ( ( `' f ` M ) e. A /\ ( A \ { ( `' f ` M ) } ) ~~ M ) -> E. x e. A ( A \ { x } ) ~~ M )
14 6 9 13 syl2anc 
 |-  ( ( M e. _om /\ f : A -1-1-onto-> suc M ) -> E. x e. A ( A \ { x } ) ~~ M )
15 14 exlimiv 
 |-  ( E. f ( M e. _om /\ f : A -1-1-onto-> suc M ) -> E. x e. A ( A \ { x } ) ~~ M )
16 2 15 sylbir 
 |-  ( ( M e. _om /\ E. f f : A -1-1-onto-> suc M ) -> E. x e. A ( A \ { x } ) ~~ M )
17 1 16 sylan2b 
 |-  ( ( M e. _om /\ A ~~ suc M ) -> E. x e. A ( A \ { x } ) ~~ M )