![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > args | Structured version Visualization version GIF version |
Description: Two ways to express the class of unique-valued arguments of 𝐹, which is the same as the domain of 𝐹 whenever 𝐹 is a function. The left-hand side of the equality is from Definition 10.2 of [Quine] p. 65. Quine uses the notation "arg 𝐹 " for this class (for which we have no separate notation). Observe the resemblance to the alternate definition dffv4 6431 of function value, which is based on the idea in Quine's definition. (Contributed by NM, 8-May-2005.) |
Ref | Expression |
---|---|
args | ⊢ {𝑥 ∣ ∃𝑦(𝐹 “ {𝑥}) = {𝑦}} = {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3418 | . . . . . 6 ⊢ 𝑥 ∈ V | |
2 | imasng 5729 | . . . . . 6 ⊢ (𝑥 ∈ V → (𝐹 “ {𝑥}) = {𝑦 ∣ 𝑥𝐹𝑦}) | |
3 | 1, 2 | ax-mp 5 | . . . . 5 ⊢ (𝐹 “ {𝑥}) = {𝑦 ∣ 𝑥𝐹𝑦} |
4 | 3 | eqeq1i 2831 | . . . 4 ⊢ ((𝐹 “ {𝑥}) = {𝑦} ↔ {𝑦 ∣ 𝑥𝐹𝑦} = {𝑦}) |
5 | 4 | exbii 1949 | . . 3 ⊢ (∃𝑦(𝐹 “ {𝑥}) = {𝑦} ↔ ∃𝑦{𝑦 ∣ 𝑥𝐹𝑦} = {𝑦}) |
6 | euabsn 4480 | . . 3 ⊢ (∃!𝑦 𝑥𝐹𝑦 ↔ ∃𝑦{𝑦 ∣ 𝑥𝐹𝑦} = {𝑦}) | |
7 | 5, 6 | bitr4i 270 | . 2 ⊢ (∃𝑦(𝐹 “ {𝑥}) = {𝑦} ↔ ∃!𝑦 𝑥𝐹𝑦) |
8 | 7 | abbii 2945 | 1 ⊢ {𝑥 ∣ ∃𝑦(𝐹 “ {𝑥}) = {𝑦}} = {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦} |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1658 ∃wex 1880 ∈ wcel 2166 ∃!weu 2640 {cab 2812 Vcvv 3415 {csn 4398 class class class wbr 4874 “ cima 5346 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-sep 5006 ax-nul 5014 ax-pr 5128 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2606 df-eu 2641 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ral 3123 df-rex 3124 df-rab 3127 df-v 3417 df-sbc 3664 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-nul 4146 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-br 4875 df-opab 4937 df-xp 5349 df-cnv 5351 df-dm 5353 df-rn 5354 df-res 5355 df-ima 5356 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |