Metamath Proof Explorer

Theorem hashrabsn1

Description: If the size of a restricted class abstraction restricted to a singleton is 1, the condition of the class abstraction must hold for the singleton. (Contributed by Alexander van der Vekens, 3-Sep-2018)

Ref Expression
Assertion hashrabsn1 
|- ( ( # ` { x e. { A } | ph } ) = 1 -> [. A / x ]. ph )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  { x e. { A } | ph } = { x e. { A } | ph }
2 rabrsn 
 |-  ( { x e. { A } | ph } = { x e. { A } | ph } -> ( { x e. { A } | ph } = (/) \/ { x e. { A } | ph } = { A } ) )
3 fveqeq2 
 |-  ( { x e. { A } | ph } = (/) -> ( ( # ` { x e. { A } | ph } ) = 1 <-> ( # ` (/) ) = 1 ) )
4 hash0 
 |-  ( # ` (/) ) = 0
5 4 eqeq1i 
 |-  ( ( # ` (/) ) = 1 <-> 0 = 1 )
6 0ne1 
 |-  0 =/= 1
7 eqneqall 
 |-  ( 0 = 1 -> ( 0 =/= 1 -> [. A / x ]. ph ) )
8 6 7 mpi 
 |-  ( 0 = 1 -> [. A / x ]. ph )
9 5 8 sylbi 
 |-  ( ( # ` (/) ) = 1 -> [. A / x ]. ph )
10 3 9 biimtrdi 
 |-  ( { x e. { A } | ph } = (/) -> ( ( # ` { x e. { A } | ph } ) = 1 -> [. A / x ]. ph ) )
11 snidg 
 |-  ( A e. _V -> A e. { A } )
12 11 adantr 
 |-  ( ( A e. _V /\ { x e. { A } | ph } = { A } ) -> A e. { A } )
13 eleq2 
 |-  ( { x e. { A } | ph } = { A } -> ( A e. { x e. { A } | ph } <-> A e. { A } ) )
14 13 adantl 
 |-  ( ( A e. _V /\ { x e. { A } | ph } = { A } ) -> ( A e. { x e. { A } | ph } <-> A e. { A } ) )
15 12 14 mpbird 
 |-  ( ( A e. _V /\ { x e. { A } | ph } = { A } ) -> A e. { x e. { A } | ph } )
16 nfcv 
 |-  F/_ x { A }
17 16 elrabsf 
 |-  ( A e. { x e. { A } | ph } <-> ( A e. { A } /\ [. A / x ]. ph ) )
18 17 simprbi 
 |-  ( A e. { x e. { A } | ph } -> [. A / x ]. ph )
19 15 18 syl 
 |-  ( ( A e. _V /\ { x e. { A } | ph } = { A } ) -> [. A / x ]. ph )
20 19 a1d 
 |-  ( ( A e. _V /\ { x e. { A } | ph } = { A } ) -> ( ( # ` { x e. { A } | ph } ) = 1 -> [. A / x ]. ph ) )
21 20 ex 
 |-  ( A e. _V -> ( { x e. { A } | ph } = { A } -> ( ( # ` { x e. { A } | ph } ) = 1 -> [. A / x ]. ph ) ) )
22 snprc 
 |-  ( -. A e. _V <-> { A } = (/) )
23 eqeq2 
 |-  ( { A } = (/) -> ( { x e. { A } | ph } = { A } <-> { x e. { A } | ph } = (/) ) )
24 ax-1ne0 
 |-  1 =/= 0
25 eqneqall 
 |-  ( 1 = 0 -> ( 1 =/= 0 -> [. A / x ]. ph ) )
26 24 25 mpi 
 |-  ( 1 = 0 -> [. A / x ]. ph )
27 26 eqcoms 
 |-  ( 0 = 1 -> [. A / x ]. ph )
28 5 27 sylbi 
 |-  ( ( # ` (/) ) = 1 -> [. A / x ]. ph )
29 3 28 biimtrdi 
 |-  ( { x e. { A } | ph } = (/) -> ( ( # ` { x e. { A } | ph } ) = 1 -> [. A / x ]. ph ) )
30 23 29 biimtrdi 
 |-  ( { A } = (/) -> ( { x e. { A } | ph } = { A } -> ( ( # ` { x e. { A } | ph } ) = 1 -> [. A / x ]. ph ) ) )
31 22 30 sylbi 
 |-  ( -. A e. _V -> ( { x e. { A } | ph } = { A } -> ( ( # ` { x e. { A } | ph } ) = 1 -> [. A / x ]. ph ) ) )
32 21 31 pm2.61i 
 |-  ( { x e. { A } | ph } = { A } -> ( ( # ` { x e. { A } | ph } ) = 1 -> [. A / x ]. ph ) )
33 10 32 jaoi 
 |-  ( ( { x e. { A } | ph } = (/) \/ { x e. { A } | ph } = { A } ) -> ( ( # ` { x e. { A } | ph } ) = 1 -> [. A / x ]. ph ) )
34 1 2 33 mp2b 
 |-  ( ( # ` { x e. { A } | ph } ) = 1 -> [. A / x ]. ph )