![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fnbrfvb | Structured version Visualization version GIF version |
Description: Equivalence of function value and binary relation. (Contributed by NM, 19-Apr-2004.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Ref | Expression |
---|---|
fnbrfvb | ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = 𝐶 ↔ 𝐵𝐹𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2736 | . . . 4 ⊢ (𝐹‘𝐵) = (𝐹‘𝐵) | |
2 | fvex 6855 | . . . . 5 ⊢ (𝐹‘𝐵) ∈ V | |
3 | eqeq2 2748 | . . . . . . 7 ⊢ (𝑥 = (𝐹‘𝐵) → ((𝐹‘𝐵) = 𝑥 ↔ (𝐹‘𝐵) = (𝐹‘𝐵))) | |
4 | breq2 5109 | . . . . . . 7 ⊢ (𝑥 = (𝐹‘𝐵) → (𝐵𝐹𝑥 ↔ 𝐵𝐹(𝐹‘𝐵))) | |
5 | 3, 4 | bibi12d 345 | . . . . . 6 ⊢ (𝑥 = (𝐹‘𝐵) → (((𝐹‘𝐵) = 𝑥 ↔ 𝐵𝐹𝑥) ↔ ((𝐹‘𝐵) = (𝐹‘𝐵) ↔ 𝐵𝐹(𝐹‘𝐵)))) |
6 | 5 | imbi2d 340 | . . . . 5 ⊢ (𝑥 = (𝐹‘𝐵) → (((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = 𝑥 ↔ 𝐵𝐹𝑥)) ↔ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = (𝐹‘𝐵) ↔ 𝐵𝐹(𝐹‘𝐵))))) |
7 | fneu 6612 | . . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ∃!𝑥 𝐵𝐹𝑥) | |
8 | tz6.12c 6864 | . . . . . 6 ⊢ (∃!𝑥 𝐵𝐹𝑥 → ((𝐹‘𝐵) = 𝑥 ↔ 𝐵𝐹𝑥)) | |
9 | 7, 8 | syl 17 | . . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = 𝑥 ↔ 𝐵𝐹𝑥)) |
10 | 2, 6, 9 | vtocl 3518 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = (𝐹‘𝐵) ↔ 𝐵𝐹(𝐹‘𝐵))) |
11 | 1, 10 | mpbii 232 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵𝐹(𝐹‘𝐵)) |
12 | breq2 5109 | . . 3 ⊢ ((𝐹‘𝐵) = 𝐶 → (𝐵𝐹(𝐹‘𝐵) ↔ 𝐵𝐹𝐶)) | |
13 | 11, 12 | syl5ibcom 244 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = 𝐶 → 𝐵𝐹𝐶)) |
14 | fnfun 6602 | . . . 4 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹) | |
15 | funbrfv 6893 | . . . 4 ⊢ (Fun 𝐹 → (𝐵𝐹𝐶 → (𝐹‘𝐵) = 𝐶)) | |
16 | 14, 15 | syl 17 | . . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵𝐹𝐶 → (𝐹‘𝐵) = 𝐶)) |
17 | 16 | adantr 481 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐵𝐹𝐶 → (𝐹‘𝐵) = 𝐶)) |
18 | 13, 17 | impbid 211 | 1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = 𝐶 ↔ 𝐵𝐹𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∃!weu 2566 class class class wbr 5105 Fun wfun 6490 Fn wfn 6491 ‘cfv 6496 |
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-12 2171 ax-ext 2707 ax-sep 5256 ax-nul 5263 ax-pr 5384 |
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-ne 2944 df-ral 3065 df-rex 3074 df-rab 3408 df-v 3447 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-br 5106 df-opab 5168 df-id 5531 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-iota 6448 df-fun 6498 df-fn 6499 df-fv 6504 |
This theorem is referenced by: fnopfvb 6896 funbrfvb 6897 fnbrfvb2 6899 dffn5 6901 feqmptdf 6912 fnsnfv 6920 fnsnfvOLD 6921 fndmdif 6992 dffo4 7053 dff13 7202 isomin 7282 isoini 7283 br1steqg 7943 br2ndeqg 7944 1stconst 8032 2ndconst 8033 fsplit 8049 seqomlem3 8398 seqomlem4 8399 nqerrel 10868 imasleval 17423 znleval 20961 scutun12 27149 madeval2 27183 axcontlem5 27917 elnlfn 30870 adjbd1o 31027 fcoinvbr 31526 fv1stcnv 34351 fv2ndcnv 34352 fvbigcup 34487 fvsingle 34505 imageval 34515 brfullfun 34533 bj-mptval 35588 unccur 36061 poimirlem2 36080 poimirlem23 36101 pw2f1ocnv 41347 brcoffn 42292 funressnfv 45267 fnbrafvb 45376 |
Copyright terms: Public domain | W3C validator |