![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fnopfvb | Structured version Visualization version GIF version |
Description: Equivalence of function value and ordered pair membership. (Contributed by NM, 7-Nov-1995.) |
Ref | Expression |
---|---|
fnopfvb | ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = 𝐶 ↔ 〈𝐵, 𝐶〉 ∈ 𝐹)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnbrfvb 6349 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = 𝐶 ↔ 𝐵𝐹𝐶)) | |
2 | df-br 4761 | . 2 ⊢ (𝐵𝐹𝐶 ↔ 〈𝐵, 𝐶〉 ∈ 𝐹) | |
3 | 1, 2 | syl6bb 276 | 1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) = 𝐶 ↔ 〈𝐵, 𝐶〉 ∈ 𝐹)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1596 ∈ wcel 2103 〈cop 4291 class class class wbr 4760 Fn wfn 5996 ‘cfv 6001 |
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-rab 3023 df-v 3306 df-sbc 3542 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-uni 4545 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-iota 5964 df-fun 6003 df-fn 6004 df-fv 6009 |
This theorem is referenced by: funopfvb 6352 fvopab3g 6391 f1ofveu 6760 fnotovbOLD 6811 ovid 6894 ov 6897 ovg 6916 wfrlem14 7548 tfrlem11 7604 rdglim2 7648 tz7.48-1 7658 mdetunilem9 20549 |
Copyright terms: Public domain | W3C validator |