![]() |
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 6836 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 | imasng 6033 | . . . . . 6 ⊢ (𝑥 ∈ V → (𝐹 “ {𝑥}) = {𝑦 ∣ 𝑥𝐹𝑦}) | |
2 | 1 | elv 3449 | . . . . 5 ⊢ (𝐹 “ {𝑥}) = {𝑦 ∣ 𝑥𝐹𝑦} |
3 | 2 | eqeq1i 2741 | . . . 4 ⊢ ((𝐹 “ {𝑥}) = {𝑦} ↔ {𝑦 ∣ 𝑥𝐹𝑦} = {𝑦}) |
4 | 3 | exbii 1850 | . . 3 ⊢ (∃𝑦(𝐹 “ {𝑥}) = {𝑦} ↔ ∃𝑦{𝑦 ∣ 𝑥𝐹𝑦} = {𝑦}) |
5 | euabsn 4685 | . . 3 ⊢ (∃!𝑦 𝑥𝐹𝑦 ↔ ∃𝑦{𝑦 ∣ 𝑥𝐹𝑦} = {𝑦}) | |
6 | 4, 5 | bitr4i 277 | . 2 ⊢ (∃𝑦(𝐹 “ {𝑥}) = {𝑦} ↔ ∃!𝑦 𝑥𝐹𝑦) |
7 | 6 | abbii 2806 | 1 ⊢ {𝑥 ∣ ∃𝑦(𝐹 “ {𝑥}) = {𝑦}} = {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦} |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 ∃wex 1781 ∃!weu 2566 {cab 2713 Vcvv 3443 {csn 4584 class class class wbr 5103 “ cima 5634 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5254 ax-nul 5261 ax-pr 5382 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-br 5104 df-opab 5166 df-xp 5637 df-cnv 5639 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |