| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > funsng | Structured version Visualization version GIF version | ||
| Description: A singleton of an ordered pair is a function. Theorem 10.5 of [Quine] p. 65. (Contributed by NM, 28-Jun-2011.) |
| Ref | Expression |
|---|---|
| funsng | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → Fun {〈𝐴, 𝐵〉}) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | funcnvsn 6527 | . 2 ⊢ Fun ◡{〈𝐵, 𝐴〉} | |
| 2 | cnvsng 6167 | . . . 4 ⊢ ((𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → ◡{〈𝐵, 𝐴〉} = {〈𝐴, 𝐵〉}) | |
| 3 | 2 | ancoms 458 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ◡{〈𝐵, 𝐴〉} = {〈𝐴, 𝐵〉}) |
| 4 | 3 | funeqd 6499 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (Fun ◡{〈𝐵, 𝐴〉} ↔ Fun {〈𝐴, 𝐵〉})) |
| 5 | 1, 4 | mpbii 233 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → Fun {〈𝐴, 𝐵〉}) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2110 {csn 4574 〈cop 4580 ◡ccnv 5613 Fun wfun 6471 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2112 ax-9 2120 ax-ext 2702 ax-sep 5232 ax-nul 5242 ax-pr 5368 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-sb 2067 df-mo 2534 df-clab 2709 df-cleq 2722 df-clel 2804 df-ral 3046 df-rex 3055 df-rab 3394 df-v 3436 df-dif 3903 df-un 3905 df-ss 3917 df-nul 4282 df-if 4474 df-sn 4575 df-pr 4577 df-op 4581 df-br 5090 df-opab 5152 df-id 5509 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-fun 6479 |
| This theorem is referenced by: fnsng 6529 funsn 6530 funprg 6531 funtpg 6532 fvsng 7109 tfrlem10 8301 snopfsupp 9270 funsnfsupp 9271 strle1 17061 setsfun 17074 setsfun0 17075 noextend 27598 p1evtxdeqlem 29484 trlsegvdeglem3 30192 bnj519 34738 bnj150 34878 |
| Copyright terms: Public domain | W3C validator |