![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fsng | Structured version Visualization version GIF version |
Description: A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 26-Oct-2012.) |
Ref | Expression |
---|---|
fsng | ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐹:{𝐴}⟶{𝐵} ↔ 𝐹 = {〈𝐴, 𝐵〉})) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sneq 4295 | . . . 4 ⊢ (𝑎 = 𝐴 → {𝑎} = {𝐴}) | |
2 | 1 | feq2d 6144 | . . 3 ⊢ (𝑎 = 𝐴 → (𝐹:{𝑎}⟶{𝑏} ↔ 𝐹:{𝐴}⟶{𝑏})) |
3 | opeq1 4509 | . . . . 5 ⊢ (𝑎 = 𝐴 → 〈𝑎, 𝑏〉 = 〈𝐴, 𝑏〉) | |
4 | 3 | sneqd 4297 | . . . 4 ⊢ (𝑎 = 𝐴 → {〈𝑎, 𝑏〉} = {〈𝐴, 𝑏〉}) |
5 | 4 | eqeq2d 2734 | . . 3 ⊢ (𝑎 = 𝐴 → (𝐹 = {〈𝑎, 𝑏〉} ↔ 𝐹 = {〈𝐴, 𝑏〉})) |
6 | 2, 5 | bibi12d 334 | . 2 ⊢ (𝑎 = 𝐴 → ((𝐹:{𝑎}⟶{𝑏} ↔ 𝐹 = {〈𝑎, 𝑏〉}) ↔ (𝐹:{𝐴}⟶{𝑏} ↔ 𝐹 = {〈𝐴, 𝑏〉}))) |
7 | sneq 4295 | . . . 4 ⊢ (𝑏 = 𝐵 → {𝑏} = {𝐵}) | |
8 | 7 | feq3d 6145 | . . 3 ⊢ (𝑏 = 𝐵 → (𝐹:{𝐴}⟶{𝑏} ↔ 𝐹:{𝐴}⟶{𝐵})) |
9 | opeq2 4510 | . . . . 5 ⊢ (𝑏 = 𝐵 → 〈𝐴, 𝑏〉 = 〈𝐴, 𝐵〉) | |
10 | 9 | sneqd 4297 | . . . 4 ⊢ (𝑏 = 𝐵 → {〈𝐴, 𝑏〉} = {〈𝐴, 𝐵〉}) |
11 | 10 | eqeq2d 2734 | . . 3 ⊢ (𝑏 = 𝐵 → (𝐹 = {〈𝐴, 𝑏〉} ↔ 𝐹 = {〈𝐴, 𝐵〉})) |
12 | 8, 11 | bibi12d 334 | . 2 ⊢ (𝑏 = 𝐵 → ((𝐹:{𝐴}⟶{𝑏} ↔ 𝐹 = {〈𝐴, 𝑏〉}) ↔ (𝐹:{𝐴}⟶{𝐵} ↔ 𝐹 = {〈𝐴, 𝐵〉}))) |
13 | vex 3307 | . . 3 ⊢ 𝑎 ∈ V | |
14 | vex 3307 | . . 3 ⊢ 𝑏 ∈ V | |
15 | 13, 14 | fsn 6517 | . 2 ⊢ (𝐹:{𝑎}⟶{𝑏} ↔ 𝐹 = {〈𝑎, 𝑏〉}) |
16 | 6, 12, 15 | vtocl2g 3374 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐹:{𝐴}⟶{𝐵} ↔ 𝐹 = {〈𝐴, 𝐵〉})) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1596 ∈ wcel 2103 {csn 4285 〈cop 4291 ⟶wf 5997 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-9 2112 ax-10 2132 ax-11 2147 ax-12 2160 ax-13 2355 ax-ext 2704 ax-sep 4889 ax-nul 4897 ax-pr 5011 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1599 df-ex 1818 df-nf 1823 df-sb 2011 df-eu 2575 df-mo 2576 df-clab 2711 df-cleq 2717 df-clel 2720 df-nfc 2855 df-ral 3019 df-rex 3020 df-reu 3021 df-rab 3023 df-v 3306 df-dif 3683 df-un 3685 df-in 3687 df-ss 3694 df-nul 4024 df-if 4195 df-sn 4286 df-pr 4288 df-op 4292 df-br 4761 df-opab 4821 df-id 5128 df-xp 5224 df-rel 5225 df-cnv 5226 df-co 5227 df-dm 5228 df-rn 5229 df-fun 6003 df-fn 6004 df-f 6005 df-f1 6006 df-fo 6007 df-f1o 6008 |
This theorem is referenced by: xpsng 6521 ftpg 6538 axdc3lem4 9388 fseq1p1m1 12528 cats1un 13596 intopsn 17375 grp1inv 17645 symg1bas 17937 esumsnf 30356 bnj149 31173 rngosn3 33955 k0004lem3 38866 mapsnd 39804 ovnovollem1 41293 mapsnop 42550 snlindsntorlem 42686 lmod1zr 42709 |
Copyright terms: Public domain | W3C validator |