![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fex2 | Structured version Visualization version GIF version |
Description: A function with bounded domain and codomain is a set. This version of fex 7209 is proven without the Axiom of Replacement ax-rep 5275, but depends on ax-un 7705, which is not required for the proof of fex 7209. (Contributed by Mario Carneiro, 24-Jun-2015.) |
Ref | Expression |
---|---|
fex2 | ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpexg 7717 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) | |
2 | 1 | 3adant1 1130 | . 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
3 | fssxp 6729 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵)) | |
4 | 3 | 3ad2ant1 1133 | . 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ⊆ (𝐴 × 𝐵)) |
5 | 2, 4 | ssexd 5314 | 1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1087 ∈ wcel 2106 Vcvv 3470 ⊆ wss 3941 × cxp 5664 ⟶wf 6525 |
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-ext 2702 ax-sep 5289 ax-nul 5296 ax-pow 5353 ax-pr 5417 ax-un 7705 |
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-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-ral 3061 df-rex 3070 df-rab 3430 df-v 3472 df-dif 3944 df-un 3946 df-in 3948 df-ss 3958 df-nul 4316 df-if 4520 df-pw 4595 df-sn 4620 df-pr 4622 df-op 4626 df-uni 4899 df-br 5139 df-opab 5201 df-xp 5672 df-rel 5673 df-cnv 5674 df-dm 5676 df-rn 5677 df-fun 6531 df-fn 6532 df-f 6533 |
This theorem is referenced by: elmapg 8813 f1oen2g 8944 f1dom2g 8945 f1dom2gOLD 8946 dom3d 8970 domssex2 9117 domssex 9118 mapxpen 9123 oismo 9514 wdomima2g 9560 dfac8clem 10006 acni2 10020 acnlem 10022 dfac4 10096 dfac2a 10103 axdc2lem 10422 axdc4lem 10429 axcclem 10431 addex 12951 mulex 12952 seqf1olem2 13987 seqf1o 13988 limsuple 15401 limsuplt 15402 limsupbnd1 15405 caucvgrlem 15598 prdsplusg 17383 prdsmulr 17384 prdsvsca 17385 prdshom 17392 gsumval 18575 frmdplusg 18707 odinf 19392 staffval 20399 cnfldcj 20880 cnfldds 20883 xrsadd 20891 xrsmul 20892 xrsds 20917 ocvfval 21147 cnpfval 22662 iscnp2 22667 fmf 23373 tsmsval 23559 blfvalps 23813 nmfval 24021 tngnm 24092 tngngp2 24093 tngngpd 24094 tngngp 24095 nmoffn 24152 nmofval 24155 ishtpy 24412 tcphex 24658 adjeu 31000 ismeas 33012 isismty 36458 rrnval 36484 |
Copyright terms: Public domain | W3C validator |