This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 )

Proof

Step Hyp Ref Expression
1 eqid ⊢ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝑥 ∈ { 𝐴 } ∣ 𝜑 }
2 rabrsn ⊢ ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } → ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = ∅ ∨ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } ) )
3 fveqeq2 ⊢ ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = ∅ → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 1 ↔ ( ♯ ‘ ∅ ) = 1 ) )
4 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
5 4 eqeq1i ⊢ ( ( ♯ ‘ ∅ ) = 1 ↔ 0 = 1 )
6 0ne1 ⊢ 0 ≠ 1
7 eqneqall ⊢ ( 0 = 1 → ( 0 ≠ 1 → [ 𝐴 / 𝑥 ] 𝜑 ) )
8 6 7 mpi ⊢ ( 0 = 1 → [ 𝐴 / 𝑥 ] 𝜑 )
9 5 8 sylbi ⊢ ( ( ♯ ‘ ∅ ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 )
10 3 9 biimtrdi ⊢ ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = ∅ → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 ) )
11 snidg ⊢ ( 𝐴 ∈ V → 𝐴 ∈ { 𝐴 } )
12 11 adantr ⊢ ( ( 𝐴 ∈ V ∧ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } ) → 𝐴 ∈ { 𝐴 } )
13 eleq2 ⊢ ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } → ( 𝐴 ∈ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ↔ 𝐴 ∈ { 𝐴 } ) )
14 13 adantl ⊢ ( ( 𝐴 ∈ V ∧ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } ) → ( 𝐴 ∈ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ↔ 𝐴 ∈ { 𝐴 } ) )
15 12 14 mpbird ⊢ ( ( 𝐴 ∈ V ∧ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } ) → 𝐴 ∈ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } )
16 nfcv ⊢ Ⅎ 𝑥 { 𝐴 }
17 16 elrabsf ⊢ ( 𝐴 ∈ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ↔ ( 𝐴 ∈ { 𝐴 } ∧ [ 𝐴 / 𝑥 ] 𝜑 ) )
18 17 simprbi ⊢ ( 𝐴 ∈ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } → [ 𝐴 / 𝑥 ] 𝜑 )
19 15 18 syl ⊢ ( ( 𝐴 ∈ V ∧ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } ) → [ 𝐴 / 𝑥 ] 𝜑 )
20 19 a1d ⊢ ( ( 𝐴 ∈ V ∧ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } ) → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 ) )
21 20 ex ⊢ ( 𝐴 ∈ V → ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 ) ) )
22 snprc ⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
23 eqeq2 ⊢ ( { 𝐴 } = ∅ → ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } ↔ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = ∅ ) )
24 ax-1ne0 ⊢ 1 ≠ 0
25 eqneqall ⊢ ( 1 = 0 → ( 1 ≠ 0 → [ 𝐴 / 𝑥 ] 𝜑 ) )
26 24 25 mpi ⊢ ( 1 = 0 → [ 𝐴 / 𝑥 ] 𝜑 )
27 26 eqcoms ⊢ ( 0 = 1 → [ 𝐴 / 𝑥 ] 𝜑 )
28 5 27 sylbi ⊢ ( ( ♯ ‘ ∅ ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 )
29 3 28 biimtrdi ⊢ ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = ∅ → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 ) )
30 23 29 biimtrdi ⊢ ( { 𝐴 } = ∅ → ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 ) ) )
31 22 30 sylbi ⊢ ( ¬ 𝐴 ∈ V → ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 ) ) )
32 21 31 pm2.61i ⊢ ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 ) )
33 10 32 jaoi ⊢ ( ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = ∅ ∨ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } ) → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 ) )
34 1 2 33 mp2b ⊢ ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 )