| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > fmpo | Structured version Visualization version GIF version | ||
| Description: Functionality, domain and range of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.) |
| Ref | Expression |
|---|---|
| fmpo.1 | ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
| Ref | Expression |
|---|---|
| fmpo | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fmpo.1 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | |
| 2 | 1 | fmpox 8070 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷) |
| 3 | iunxpconst 5736 | . . 3 ⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵) | |
| 4 | 3 | feq2i 6701 | . 2 ⊢ (𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷) |
| 5 | 2, 4 | bitri 278 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: ↔ wb 209 = wceq 1570 ∈ wcel 2146 ∀wral 3081 {csn 4591 ∪ ciun 4958 × cxp 5661 ⟶wf 6536 ∈ cmpo 7421 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-sep 5259 ax-nul 5271 ax-pr 5406 ax-un 7742 |
| This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3082 df-rex 3092 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-if 4490 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-id 5558 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-fv 6548 df-oprab 7423 df-mpo 7424 df-1st 7992 df-2nd 7993 |
| This theorem is used by: fnmpo 8072 ovmpoelrn 8075 fmpoco 8096 eroprf 8819 omxpenlem 9073 mapxpen 9138 dffi3 9398 ixpiunwdom 9559 cantnfvalf 9641 iunfictbso 10114 axdc4lem 10454 axcclem 10456 addpqf 10944 mulpqf 10946 subf 11474 xaddf 13266 xmulf 13314 ixxf 13398 ioof 13490 fzf 13555 fzof 13701 axdc4uzlem 14037 sadcf 16533 smupf 16558 gcdf 16592 eucalgf 16663 vdwapf 17054 prdsplusg 17533 prdsmulr 17534 prdsvsca 17535 prdshom 17542 imasvscaf 17615 xpsff1o 17643 wunnat 18038 catcoppccl 18196 catcfuccl 18197 catcxpccl 18285 evlfcl 18300 hofcl 18337 mgmplusf 18730 grpsubf 19129 subgga 19414 lactghmga 19519 sylow1lem2 19713 sylow3lem1 19741 lsmssv 19757 smndlsmidm 19770 efgmf 19827 efgtf 19836 frgpuptf 19884 lmodscaf 21055 xrsds 21610 phlipf 21852 evlslem2 22280 mamucl 22608 matbas2d 22630 mamumat1cl 22646 ordtbas2 23398 iccordt 23421 txuni2 23773 xkotf 23793 txbasval 23814 tx1stc 23858 xkococn 23868 cnmpt12 23875 cnmpt21 23879 cnmpt2t 23881 cnmpt22 23882 cnmptcom 23886 cnmpt2k 23896 txswaphmeo 24013 xpstopnlem1 24017 cnmpt2plusg 24296 cnmpt2vsca 24403 prdsdsf 24575 blfvalps 24591 blfps 24614 blf 24615 stdbdmet 24724 met2ndci 24730 dscmet 24780 xrsxmet 25018 cnmpt2ds 25052 cnmpopc 25138 iimulcn 25148 ishtpy 25182 reparphti 25207 cnmpt2ip 25458 bcthlem5 25538 rrxmet 25618 dyadf 25801 itg1addlem2 25907 mbfi1fseqlem1 25925 mbfi1fseqlem3 25927 mbfi1fseqlem4 25928 mbfi1fseqlem5 25929 cxpcn3 26964 sgmf 27360 subsf 28308 midf 29136 grpodivf 30961 nvmf 31068 ipf 31136 hvsubf 31438 ofoprabco 33080 suppovss 33097 elrgspnlem2 33627 fedgmullem1 34083 fedgmullem2 34084 fedgmul 34085 sitmf 34807 cvxsconn 35772 cvmlift2lem5 35836 uncf 38307 mblfinlem1 38365 mblfinlem2 38366 sdclem1 38452 metf1o 38464 rrnval 38536 rrnmet 38538 aks6d1c3 42948 fmpocos 43062 resubf 43200 sn-subf 43248 evlselv 43379 frmx 43698 frmy 43699 ofoafg 44139 naddcnff 44147 mnringmulrcld 45010 icof 45993 fmpodg 49704 rescofuf 49928 |
| Copyright terms: Public domain | W3C validator |