Metamath Proof Explorer

Theorem bj-snsetex

Description: The class of sets "whose singletons" belong to a set is a set. Nice application of ax-rep . (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion bj-snsetex 
|- ( A e. V -> { x | { x } e. A } e. _V )

Proof

Step Hyp Ref Expression
1 elisset 
 |-  ( A e. V -> E. y y = A )
2 eleq2 
 |-  ( y = A -> ( { x } e. y <-> { x } e. A ) )
3 2 abbidv 
 |-  ( y = A -> { x | { x } e. y } = { x | { x } e. A } )
4 eleq1 
 |-  ( { x | { x } e. y } = { x | { x } e. A } -> ( { x | { x } e. y } e. _V <-> { x | { x } e. A } e. _V ) )
5 4 biimpd 
 |-  ( { x | { x } e. y } = { x | { x } e. A } -> ( { x | { x } e. y } e. _V -> { x | { x } e. A } e. _V ) )
6 3 5 syl 
 |-  ( y = A -> ( { x | { x } e. y } e. _V -> { x | { x } e. A } e. _V ) )
7 6 eximi 
 |-  ( E. y y = A -> E. y ( { x | { x } e. y } e. _V -> { x | { x } e. A } e. _V ) )
8 1 7 syl 
 |-  ( A e. V -> E. y ( { x | { x } e. y } e. _V -> { x | { x } e. A } e. _V ) )
9 bj-eximcom 
 |-  ( E. y ( { x | { x } e. y } e. _V -> { x | { x } e. A } e. _V ) -> ( A. y { x | { x } e. y } e. _V -> E. y { x | { x } e. A } e. _V ) )
10 9 com12 
 |-  ( A. y { x | { x } e. y } e. _V -> ( E. y ( { x | { x } e. y } e. _V -> { x | { x } e. A } e. _V ) -> E. y { x | { x } e. A } e. _V ) )
11 ax-rep 
 |-  ( A. u E. z A. t ( A. z u = { t } -> t = z ) -> E. z A. t ( t e. z <-> E. u ( u e. y /\ A. z u = { t } ) ) )
12 19.3v 
 |-  ( A. z u = { t } <-> u = { t } )
13 12 sbbii 
 |-  ( [ z / t ] A. z u = { t } <-> [ z / t ] u = { t } )
14 sbsbc 
 |-  ( [ z / t ] u = { t } <-> [. z / t ]. u = { t } )
15 sbceq2g 
 |-  ( z e. _V -> ( [. z / t ]. u = { t } <-> u = [_ z / t ]_ { t } ) )
16 15 elv 
 |-  ( [. z / t ]. u = { t } <-> u = [_ z / t ]_ { t } )
17 14 16 bitri 
 |-  ( [ z / t ] u = { t } <-> u = [_ z / t ]_ { t } )
18 bj-csbsn 
 |-  [_ z / t ]_ { t } = { z }
19 18 eqeq2i 
 |-  ( u = [_ z / t ]_ { t } <-> u = { z } )
20 17 19 bitri 
 |-  ( [ z / t ] u = { t } <-> u = { z } )
21 eqtr2 
 |-  ( ( u = { t } /\ u = { z } ) -> { t } = { z } )
22 vex 
 |-  t e. _V
23 22 sneqr 
 |-  ( { t } = { z } -> t = z )
24 21 23 syl 
 |-  ( ( u = { t } /\ u = { z } ) -> t = z )
25 20 24 sylan2b 
 |-  ( ( u = { t } /\ [ z / t ] u = { t } ) -> t = z )
26 12 13 25 syl2anb 
 |-  ( ( A. z u = { t } /\ [ z / t ] A. z u = { t } ) -> t = z )
27 26 gen2 
 |-  A. t A. z ( ( A. z u = { t } /\ [ z / t ] A. z u = { t } ) -> t = z )
28 nfa1 
 |-  F/ z A. z u = { t }
29 28 mo 
 |-  ( E. z A. t ( A. z u = { t } -> t = z ) <-> A. t A. z ( ( A. z u = { t } /\ [ z / t ] A. z u = { t } ) -> t = z ) )
30 27 29 mpbir 
 |-  E. z A. t ( A. z u = { t } -> t = z )
31 11 30 mpg 
 |-  E. z A. t ( t e. z <-> E. u ( u e. y /\ A. z u = { t } ) )
32 bj-sbel1 
 |-  ( [ t / x ] { x } e. y <-> [_ t / x ]_ { x } e. y )
33 bj-csbsn 
 |-  [_ t / x ]_ { x } = { t }
34 33 eleq1i 
 |-  ( [_ t / x ]_ { x } e. y <-> { t } e. y )
35 32 34 bitri 
 |-  ( [ t / x ] { x } e. y <-> { t } e. y )
36 df-clab 
 |-  ( t e. { x | { x } e. y } <-> [ t / x ] { x } e. y )
37 12 anbi2i 
 |-  ( ( u e. y /\ A. z u = { t } ) <-> ( u e. y /\ u = { t } ) )
38 eleq1a 
 |-  ( u e. y -> ( { t } = u -> { t } e. y ) )
39 38 com12 
 |-  ( { t } = u -> ( u e. y -> { t } e. y ) )
40 39 eqcoms 
 |-  ( u = { t } -> ( u e. y -> { t } e. y ) )
41 40 imdistanri 
 |-  ( ( u e. y /\ u = { t } ) -> ( { t } e. y /\ u = { t } ) )
42 eleq1a 
 |-  ( { t } e. y -> ( u = { t } -> u e. y ) )
43 42 impac 
 |-  ( ( { t } e. y /\ u = { t } ) -> ( u e. y /\ u = { t } ) )
44 41 43 impbii 
 |-  ( ( u e. y /\ u = { t } ) <-> ( { t } e. y /\ u = { t } ) )
45 37 44 bitri 
 |-  ( ( u e. y /\ A. z u = { t } ) <-> ( { t } e. y /\ u = { t } ) )
46 45 exbii 
 |-  ( E. u ( u e. y /\ A. z u = { t } ) <-> E. u ( { t } e. y /\ u = { t } ) )
47 snex 
 |-  { t } e. _V
48 47 isseti 
 |-  E. u u = { t }
49 19.42v 
 |-  ( E. u ( { t } e. y /\ u = { t } ) <-> ( { t } e. y /\ E. u u = { t } ) )
50 48 49 mpbiran2 
 |-  ( E. u ( { t } e. y /\ u = { t } ) <-> { t } e. y )
51 46 50 bitri 
 |-  ( E. u ( u e. y /\ A. z u = { t } ) <-> { t } e. y )
52 35 36 51 3bitr4ri 
 |-  ( E. u ( u e. y /\ A. z u = { t } ) <-> t e. { x | { x } e. y } )
53 52 bibi2i 
 |-  ( ( t e. z <-> E. u ( u e. y /\ A. z u = { t } ) ) <-> ( t e. z <-> t e. { x | { x } e. y } ) )
54 53 albii 
 |-  ( A. t ( t e. z <-> E. u ( u e. y /\ A. z u = { t } ) ) <-> A. t ( t e. z <-> t e. { x | { x } e. y } ) )
55 54 exbii 
 |-  ( E. z A. t ( t e. z <-> E. u ( u e. y /\ A. z u = { t } ) ) <-> E. z A. t ( t e. z <-> t e. { x | { x } e. y } ) )
56 31 55 mpbi 
 |-  E. z A. t ( t e. z <-> t e. { x | { x } e. y } )
57 dfcleq 
 |-  ( z = { x | { x } e. y } <-> A. t ( t e. z <-> t e. { x | { x } e. y } ) )
58 57 exbii 
 |-  ( E. z z = { x | { x } e. y } <-> E. z A. t ( t e. z <-> t e. { x | { x } e. y } ) )
59 56 58 mpbir 
 |-  E. z z = { x | { x } e. y }
60 59 issetri 
 |-  { x | { x } e. y } e. _V
61 10 60 mpg 
 |-  ( E. y ( { x | { x } e. y } e. _V -> { x | { x } e. A } e. _V ) -> E. y { x | { x } e. A } e. _V )
62 8 61 syl 
 |-  ( A e. V -> E. y { x | { x } e. A } e. _V )
63 ax5e 
 |-  ( E. y { x | { x } e. A } e. _V -> { x | { x } e. A } e. _V )
64 62 63 syl 
 |-  ( A e. V -> { x | { x } e. A } e. _V )