Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fniniseg | Structured version Visualization version GIF version |
Description: Membership in the preimage of a singleton, under a function. (Contributed by Mario Carneiro, 12-May-2014.) (Proof shortened by Mario Carneiro , 28-Apr-2015.) |
Ref | Expression |
---|---|
fniniseg | ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpreima 6878 | . 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵}))) | |
2 | fvex 6730 | . . . 4 ⊢ (𝐹‘𝐶) ∈ V | |
3 | 2 | elsn 4556 | . . 3 ⊢ ((𝐹‘𝐶) ∈ {𝐵} ↔ (𝐹‘𝐶) = 𝐵) |
4 | 3 | anbi2i 626 | . 2 ⊢ ((𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵)) |
5 | 1, 4 | bitrdi 290 | 1 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1543 ∈ wcel 2110 {csn 4541 ◡ccnv 5550 “ cima 5554 Fn wfn 6375 ‘cfv 6380 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-sep 5192 ax-nul 5199 ax-pr 5322 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3410 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-nul 4238 df-if 4440 df-sn 4542 df-pr 4544 df-op 4548 df-uni 4820 df-br 5054 df-opab 5116 df-id 5455 df-xp 5557 df-rel 5558 df-cnv 5559 df-co 5560 df-dm 5561 df-rn 5562 df-res 5563 df-ima 5564 df-iota 6338 df-fun 6382 df-fn 6383 df-fv 6388 |
This theorem is referenced by: fparlem1 7880 fparlem2 7881 pw2f1olem 8749 recmulnq 10578 dmrecnq 10582 vdwlem1 16534 vdwlem2 16535 vdwlem6 16539 vdwlem8 16541 vdwlem9 16542 vdwlem12 16545 vdwlem13 16546 ramval 16561 ramub1lem1 16579 ghmeqker 18649 efgrelexlemb 19140 efgredeu 19142 psgnevpmb 20549 qtopeu 22613 itg1addlem1 24589 i1faddlem 24590 i1fmullem 24591 i1fmulclem 24600 i1fres 24603 itg10a 24608 itg1ge0a 24609 itg1climres 24612 mbfi1fseqlem4 24616 ply1remlem 25060 ply1rem 25061 fta1glem1 25063 fta1glem2 25064 fta1g 25065 fta1blem 25066 plyco0 25086 ofmulrt 25175 plyremlem 25197 plyrem 25198 fta1lem 25200 fta1 25201 vieta1lem1 25203 vieta1lem2 25204 vieta1 25205 plyexmo 25206 elaa 25209 aannenlem1 25221 aalioulem2 25226 pilem1 25343 efif1olem3 25433 efif1olem4 25434 efifo 25436 eff1olem 25437 basellem4 25966 lgsqrlem2 26228 lgsqrlem3 26229 rpvmasum2 26393 dirith 26410 foresf1o 30569 ofpreima 30722 fnpreimac 30728 1stpreimas 30758 s3clhash 30942 pwrssmgc 30997 cycpmconjslem2 31141 cyc3conja 31143 dimkerim 31422 locfinreflem 31504 qqhre 31682 indpi1 31700 indpreima 31705 sibfof 32019 cvmliftlem6 32965 cvmliftlem7 32966 cvmliftlem8 32967 cvmliftlem9 32968 taupilem3 35224 itg2addnclem 35565 itg2addnclem2 35566 pw2f1o2val2 40565 dnnumch3 40575 proot1mul 40727 proot1hash 40728 proot1ex 40729 wessf1ornlem 42395 preimafvsnel 44504 uniimaprimaeqfv 44507 elsetpreimafvbi 44516 |
Copyright terms: Public domain | W3C validator |