![]() |
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 7173 is proven without the Axiom of Replacement ax-rep 5241, but depends on ax-un 7669, which is not required for the proof of fex 7173. (Contributed by Mario Carneiro, 24-Jun-2015.) |
Ref | Expression |
---|---|
fex2 | ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpexg 7681 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) | |
2 | 1 | 3adant1 1130 | . 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
3 | fssxp 6694 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵)) | |
4 | 3 | 3ad2ant1 1133 | . 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ⊆ (𝐴 × 𝐵)) |
5 | 2, 4 | ssexd 5280 | 1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐹 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1087 ∈ wcel 2106 Vcvv 3444 ⊆ wss 3909 × cxp 5630 ⟶wf 6490 |
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 2707 ax-sep 5255 ax-nul 5262 ax-pow 5319 ax-pr 5383 ax-un 7669 |
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 2714 df-cleq 2728 df-clel 2814 df-ral 3064 df-rex 3073 df-rab 3407 df-v 3446 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-br 5105 df-opab 5167 df-xp 5638 df-rel 5639 df-cnv 5640 df-dm 5642 df-rn 5643 df-fun 6496 df-fn 6497 df-f 6498 |
This theorem is referenced by: elmapg 8775 f1oen2g 8905 f1dom2g 8906 f1dom2gOLD 8907 dom3d 8931 domssex2 9078 domssex 9079 mapxpen 9084 oismo 9473 wdomima2g 9519 dfac8clem 9965 acni2 9979 acnlem 9981 dfac4 10055 dfac2a 10062 axdc2lem 10381 axdc4lem 10388 axcclem 10390 addex 12910 mulex 12911 seqf1olem2 13945 seqf1o 13946 limsuple 15357 limsuplt 15358 limsupbnd1 15361 caucvgrlem 15554 prdsplusg 17337 prdsmulr 17338 prdsvsca 17339 prdshom 17346 gsumval 18529 frmdplusg 18661 odinf 19341 staffval 20302 cnfldcj 20799 cnfldds 20802 xrsadd 20810 xrsmul 20811 xrsds 20836 ocvfval 21066 cnpfval 22581 iscnp2 22586 fmf 23292 tsmsval 23478 blfvalps 23732 nmfval 23940 tngnm 24011 tngngp2 24012 tngngpd 24013 tngngp 24014 nmoffn 24071 nmofval 24074 ishtpy 24331 tcphex 24577 adjeu 30729 ismeas 32689 isismty 36249 rrnval 36275 |
Copyright terms: Public domain | W3C validator |