|   | 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 8093 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷) | 
| 3 | iunxpconst 5757 | . . 3 ⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵) | |
| 4 | 3 | feq2i 6727 | . 2 ⊢ (𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷) | 
| 5 | 2, 4 | bitri 275 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 = wceq 1539 ∈ wcel 2107 ∀wral 3060 {csn 4625 ∪ ciun 4990 × cxp 5682 ⟶wf 6556 ∈ cmpo 7434 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-sep 5295 ax-nul 5305 ax-pr 5431 ax-un 7756 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ral 3061 df-rex 3070 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-nul 4333 df-if 4525 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4907 df-iun 4992 df-br 5143 df-opab 5205 df-mpt 5225 df-id 5577 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-iota 6513 df-fun 6562 df-fn 6563 df-f 6564 df-fv 6568 df-oprab 7436 df-mpo 7437 df-1st 8015 df-2nd 8016 | 
| This theorem is referenced by: fnmpo 8095 ovmpoelrn 8098 fmpoco 8121 eroprf 8856 omxpenlem 9114 mapxpen 9184 dffi3 9472 ixpiunwdom 9631 cantnfvalf 9706 iunfictbso 10155 axdc4lem 10496 axcclem 10498 addpqf 10985 mulpqf 10987 subf 11511 xaddf 13267 xmulf 13315 ixxf 13398 ioof 13488 fzf 13552 fzof 13697 axdc4uzlem 14025 sadcf 16491 smupf 16516 gcdf 16550 eucalgf 16621 vdwapf 17011 prdsplusg 17504 prdsmulr 17505 prdsvsca 17506 prdshom 17513 imasvscaf 17585 xpsff1o 17613 wunnat 18005 catcoppccl 18163 catcfuccl 18164 catcxpccl 18253 evlfcl 18268 hofcl 18305 mgmplusf 18664 grpsubf 19038 subgga 19319 lactghmga 19424 sylow1lem2 19618 sylow3lem1 19646 lsmssv 19662 smndlsmidm 19675 efgmf 19732 efgtf 19741 frgpuptf 19789 lmodscaf 20883 xrsds 21428 phlipf 21671 evlslem2 22104 mamucl 22406 matbas2d 22430 mamumat1cl 22446 ordtbas2 23200 iccordt 23223 txuni2 23574 xkotf 23594 txbasval 23615 tx1stc 23659 xkococn 23669 cnmpt12 23676 cnmpt21 23680 cnmpt2t 23682 cnmpt22 23683 cnmptcom 23687 cnmpt2k 23697 txswaphmeo 23814 xpstopnlem1 23818 cnmpt2plusg 24097 cnmpt2vsca 24204 prdsdsf 24378 blfvalps 24394 blfps 24417 blf 24418 stdbdmet 24530 met2ndci 24536 dscmet 24586 xrsxmet 24832 cnmpt2ds 24866 cnmpopc 24956 iimulcn 24968 iimulcnOLD 24969 ishtpy 25005 reparphti 25030 reparphtiOLD 25031 cnmpt2ip 25283 bcthlem5 25363 rrxmet 25443 dyadf 25627 itg1addlem2 25733 mbfi1fseqlem1 25751 mbfi1fseqlem3 25753 mbfi1fseqlem4 25754 mbfi1fseqlem5 25755 cxpcn3 26792 sgmf 27189 subsf 28095 midf 28785 grpodivf 30558 nvmf 30665 ipf 30733 hvsubf 31035 ofoprabco 32675 suppovss 32691 elrgspnlem2 33248 fedgmullem1 33681 fedgmullem2 33682 fedgmul 33683 sitmf 34355 cvxsconn 35249 cvmlift2lem5 35313 uncf 37607 mblfinlem1 37665 mblfinlem2 37666 sdclem1 37751 metf1o 37763 rrnval 37835 rrnmet 37837 aks6d1c3 42125 fmpocos 42275 resubf 42416 sn-subf 42463 evlselv 42602 frmx 42930 frmy 42931 ofoafg 43372 naddcnff 43380 mnringmulrcld 44252 icof 45229 fmpodg 48775 rescofuf 48940 | 
| Copyright terms: Public domain | W3C validator |