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 6103 | . 2 ⊢ dom 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝐶 ∈ V} |
3 | dmmptd.c | . . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉) | |
4 | 3 | elexd 3428 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ V) |
5 | 4 | ralrimiva 3105 | . . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝐶 ∈ V) |
6 | rabid2 3293 | . . 3 ⊢ (𝐵 = {𝑥 ∈ 𝐵 ∣ 𝐶 ∈ V} ↔ ∀𝑥 ∈ 𝐵 𝐶 ∈ V) | |
7 | 5, 6 | sylibr 237 | . 2 ⊢ (𝜑 → 𝐵 = {𝑥 ∈ 𝐵 ∣ 𝐶 ∈ V}) |
8 | 2, 7 | eqtr4id 2797 | 1 ⊢ (𝜑 → dom 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1543 ∈ wcel 2110 ∀wral 3061 {crab 3065 Vcvv 3408 ↦ cmpt 5135 dom cdm 5551 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-sep 5192 ax-nul 5199 ax-pr 5322 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ral 3066 df-rab 3070 df-v 3410 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-nul 4238 df-if 4440 df-sn 4542 df-pr 4544 df-op 4548 df-br 5054 df-opab 5116 df-mpt 5136 df-xp 5557 df-rel 5558 df-cnv 5559 df-dm 5561 df-rn 5562 df-res 5563 df-ima 5564 |
This theorem is referenced by: lo1eq 15129 rlimeq 15130 rlimcld2 15139 rlimcn3 15151 rlimmptrcl 15169 rlimsqzlem 15212 dprdz 19417 alexsublem 22941 cmetcaulem 24185 minveclem3b 24325 mbfneg 24547 mbfsup 24561 mbfinf 24562 mbflimsup 24563 itg2monolem1 24648 itg2mono 24651 itg2i1fseq2 24654 itg2cnlem1 24659 isibl2 24664 iblcnlem 24686 limccnp2 24789 limcco 24790 dvmptres3 24853 itgsubstlem 24945 iblulm 25299 rlimcnp2 25849 dchrisumlema 26369 htthlem 28998 expgrowth 41626 mptelpm 42385 choicefi 42413 mullimc 42832 limcmptdm 42851 dvsinax 43129 dirkercncflem2 43320 fourierdlem62 43384 psmeasure 43684 ovnovollem2 43870 smfmbfcex 43967 smflimsuplem2 44026 |
Copyright terms: Public domain | W3C validator |