![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fndmexd | Structured version Visualization version GIF version |
Description: If a function is a set, its domain is a set. (Contributed by Rohan Ridenour, 13-May-2024.) |
Ref | Expression |
---|---|
fndmexd.1 | ⊢ (𝜑 → 𝐹 ∈ 𝑉) |
fndmexd.2 | ⊢ (𝜑 → 𝐹 Fn 𝐷) |
Ref | Expression |
---|---|
fndmexd | ⊢ (𝜑 → 𝐷 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fndmexd.2 | . . 3 ⊢ (𝜑 → 𝐹 Fn 𝐷) | |
2 | 1 | fndmd 6431 | . 2 ⊢ (𝜑 → dom 𝐹 = 𝐷) |
3 | fndmexd.1 | . . 3 ⊢ (𝜑 → 𝐹 ∈ 𝑉) | |
4 | 3 | dmexd 7608 | . 2 ⊢ (𝜑 → dom 𝐹 ∈ V) |
5 | 2, 4 | eqeltrrd 2852 | 1 ⊢ (𝜑 → 𝐷 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2112 Vcvv 3407 dom cdm 5517 Fn wfn 6323 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-ext 2730 ax-sep 5162 ax-nul 5169 ax-pr 5291 ax-un 7452 |
This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3an 1087 df-tru 1542 df-ex 1783 df-sb 2071 df-clab 2737 df-cleq 2751 df-clel 2831 df-rab 3077 df-v 3409 df-dif 3857 df-un 3859 df-in 3861 df-ss 3871 df-nul 4222 df-if 4414 df-sn 4516 df-pr 4518 df-op 4522 df-uni 4792 df-br 5026 df-opab 5088 df-cnv 5525 df-dm 5527 df-rn 5528 df-fn 6331 |
This theorem is referenced by: fndmexb 7611 fsetdmprc0 8435 psrbagfsupp 20667 psrbaglecl 20673 psrbagaddcl 20675 psrbagcon 20677 psrbagconf1o 20683 gsumbagdiaglem 20688 psrass1lem 20690 psrbagev1 20823 psrbagev2 20825 tdeglem1 24740 tdeglem3 24742 tdeglem4 24744 gsumhashmul 30827 finnzfsuppd 41273 |
Copyright terms: Public domain | W3C validator |