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 ∈ A | φ = 1 → [˙A / x]˙ φ

Proof

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