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