Metamath Proof Explorer

Theorem tz6.12-2

Description: Function value when F is not a function. Theorem 6.12(2) of TakeutiZaring p. 27. (Contributed by NM, 30-Apr-2004) (Proof shortened by Mario Carneiro, 31-Aug-2015) Avoid ax-10 , ax-11 , ax-12 . (Revised by TM, 25-Jan-2026)

Ref Expression
Assertion tz6.12-2 ⊢ ¬ ∃! x A F x → F ⁡ A = ∅

Proof

Step Hyp Ref Expression
1 df-fv ⊢ F ⁡ A = ι y | A F y
2 eu6im ⊢ ∃ z ∀ x A F x ↔ x = z → ∃! x A F x
3 breq2 ⊢ y = x → A F y ↔ A F x
4 3 eqabcbw ⊢ y | A F y = z ↔ ∀ x A F x ↔ x ∈ z
5 velsn ⊢ x ∈ z ↔ x = z
6 5 bibi2i ⊢ A F x ↔ x ∈ z ↔ A F x ↔ x = z
7 6 albii ⊢ ∀ x A F x ↔ x ∈ z ↔ ∀ x A F x ↔ x = z
8 4 7 bitri ⊢ y | A F y = z ↔ ∀ x A F x ↔ x = z
9 8 exbii ⊢ ∃ z y | A F y = z ↔ ∃ z ∀ x A F x ↔ x = z
10 iotanul2 ⊢ ¬ ∃ z y | A F y = z → ι y | A F y = ∅
11 9 10 sylnbir ⊢ ¬ ∃ z ∀ x A F x ↔ x = z → ι y | A F y = ∅
12 2 11 nsyl5 ⊢ ¬ ∃! x A F x → ι y | A F y = ∅
13 1 12 eqtrid ⊢ ¬ ∃! x A F x → F ⁡ A = ∅