| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > dmmptd | Structured version Visualization version GIF version | ||
| Description: The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| Ref | Expression |
|---|---|
| dmmptd.a | ⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶) |
| dmmptd.c | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉) |
| Ref | Expression |
|---|---|
| dmmptd | ⊢ (𝜑 → dom 𝐴 = 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dmmptd.a | . . 3 ⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶) | |
| 2 | 1 | dmmpt 6242 | . 2 ⊢ dom 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝐶 ∈ V} |
| 3 | dmmptd.c | . . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉) | |
| 4 | 3 | elexd 3486 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ V) |
| 5 | 4 | ralrimiva 3163 | . . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝐶 ∈ V) |
| 6 | rabid2 3456 | . . 3 ⊢ (𝐵 = {𝑥 ∈ 𝐵 ∣ 𝐶 ∈ V} ↔ ∀𝑥 ∈ 𝐵 𝐶 ∈ V) | |
| 7 | 5, 6 | sylibr 237 | . 2 ⊢ (𝜑 → 𝐵 = {𝑥 ∈ 𝐵 ∣ 𝐶 ∈ V}) |
| 8 | 2, 7 | eqtr4id 2823 | 1 ⊢ (𝜑 → dom 𝐴 = 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 400 = wceq 1567 ∈ wcel 2149 ∀wral 3085 {crab 3423 Vcvv 3463 ↦ cmpt 5196 dom cdm 5662 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5261 ax-pr 5405 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ral 3086 df-rab 3424 df-v 3465 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4493 df-sn 4595 df-pr 4597 df-op 4601 df-br 5114 df-opab 5178 df-mpt 5197 df-xp 5668 df-rel 5669 df-cnv 5670 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 |
| This theorem is referenced by: lo1eq 15618 rlimeq 15619 rlimcld2 15628 rlimcn3 15640 rlimmptrcl 15658 rlimsqzlem 15699 dprdz 20101 alexsublem 24169 cmetcaulem 25415 minveclem3b 25555 mbfneg 25777 mbfsup 25791 mbfinf 25792 mbflimsup 25793 itg2monolem1 25877 itg2mono 25880 itg2i1fseq2 25883 itg2cnlem1 25888 isibl2 25893 iblcnlem 25916 limccnp2 26019 limcco 26020 dvmptres3 26083 itgsubstlem 26175 iblulm 26535 rlimcnp2 27096 dchrisumlema 27617 htthlem 31209 qusrn 33661 esplyfvaln 33908 extdgfialglem1 34026 algextdeglem4 34054 dmqmap 38991 expgrowth 44936 mptelpm 45785 choicefi 45808 mullimc 46223 limcmptdm 46240 dvsinax 46518 dirkercncflem2 46709 fourierdlem62 46773 psmeasure 47076 ovnovollem2 47262 smfmbfcex 47365 smflimsuplem2 47426 |
| Copyright terms: Public domain | W3C validator |