Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fmpt2 | 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 |
---|---|
fmpt2.1 | ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
Ref | Expression |
---|---|
fmpt2 | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fmpt2.1 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | |
2 | 1 | fmpt2x 7125 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷) |
3 | iunxpconst 5098 | . . 3 ⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵) | |
4 | 3 | feq2i 5950 | . 2 ⊢ (𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷) |
5 | 2, 4 | bitri 263 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 = wceq 1475 ∈ wcel 1977 ∀wral 2896 {csn 4125 ∪ ciun 4455 × cxp 5036 ⟶wf 5800 ↦ cmpt2 6551 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-fv 5812 df-oprab 6553 df-mpt2 6554 df-1st 7059 df-2nd 7060 |
This theorem is referenced by: fnmpt2 7127 ovmpt2elrn 7130 fmpt2co 7147 eroprf 7732 omxpenlem 7946 mapxpen 8011 dffi3 8220 ixpiunwdom 8379 cantnfvalf 8445 iunfictbso 8820 axdc4lem 9160 axcclem 9162 addpqf 9645 mulpqf 9647 subf 10162 xaddf 11929 xmulf 11974 ixxf 12056 ioof 12142 fzf 12201 fzof 12336 axdc4uzlem 12644 sadcf 15013 smupf 15038 gcdf 15072 eucalgf 15134 vdwapf 15514 prdsval 15938 prdsplusg 15941 prdsmulr 15942 prdsvsca 15943 prdsds 15947 prdshom 15950 imasvscaf 16022 xpsff1o 16051 wunnat 16439 catcoppccl 16581 catcfuccl 16582 catcxpccl 16670 evlfcl 16685 hofcl 16722 plusffval 17070 mgmplusf 17074 grpsubf 17317 subgga 17556 lactghmga 17647 sylow1lem2 17837 sylow3lem1 17865 lsmssv 17881 lsmidm 17900 efgmf 17949 efgtf 17958 frgpuptf 18006 scaffval 18704 lmodscaf 18708 evlslem2 19333 xrsds 19608 ipffval 19812 phlipf 19816 mamucl 20026 matbas2d 20048 mamumat1cl 20064 ordtbas2 20805 iccordt 20828 txuni2 21178 xkotf 21198 txbasval 21219 tx1stc 21263 xkococn 21273 cnmpt12 21280 cnmpt21 21284 cnmpt2t 21286 cnmpt22 21287 cnmptcom 21291 cnmpt2k 21301 txswaphmeo 21418 xpstopnlem1 21422 cnmpt2plusg 21702 cnmpt2vsca 21808 prdsdsf 21982 blfvalps 21998 blfps 22021 blf 22022 stdbdmet 22131 met2ndci 22137 dscmet 22187 xrsxmet 22420 cnmpt2ds 22454 cnmpt2pc 22535 iimulcn 22545 ishtpy 22579 reparphti 22605 cnmpt2ip 22855 bcthlem5 22933 rrxmet 22999 dyadf 23165 itg1addlem2 23270 mbfi1fseqlem1 23288 mbfi1fseqlem3 23290 mbfi1fseqlem4 23291 mbfi1fseqlem5 23292 cxpcn3 24289 sgmf 24671 midf 25468 grpodivf 26776 nvmf 26884 ipf 26952 hvsubf 27256 ofoprabco 28847 sitmf 29741 sseqfv2 29783 cvxscon 30479 cvmlift2lem5 30543 uncf 32558 mblfinlem1 32616 mblfinlem2 32617 sdclem1 32709 metf1o 32721 rrnval 32796 rrnmet 32798 frmx 36496 frmy 36497 icof 38406 |
Copyright terms: Public domain | W3C validator |