MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmmptd Structured version   Visualization version   GIF version

Theorem dmmptd 6486
Description: The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
dmmptd.a 𝐴 = (𝑥𝐵𝐶)
dmmptd.c ((𝜑𝑥𝐵) → 𝐶𝑉)
Assertion
Ref Expression
dmmptd (𝜑 → dom 𝐴 = 𝐵)
Distinct variable groups:   𝑥,𝐵   𝜑,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝐶(𝑥)   𝑉(𝑥)

Proof of Theorem dmmptd
StepHypRef Expression
1 dmmptd.c . . . . 5 ((𝜑𝑥𝐵) → 𝐶𝑉)
21elexd 3512 . . . 4 ((𝜑𝑥𝐵) → 𝐶 ∈ V)
32ralrimiva 3179 . . 3 (𝜑 → ∀𝑥𝐵 𝐶 ∈ V)
4 rabid2 3379 . . 3 (𝐵 = {𝑥𝐵𝐶 ∈ V} ↔ ∀𝑥𝐵 𝐶 ∈ V)
53, 4sylibr 235 . 2 (𝜑𝐵 = {𝑥𝐵𝐶 ∈ V})
6 dmmptd.a . . 3 𝐴 = (𝑥𝐵𝐶)
76dmmpt 6087 . 2 dom 𝐴 = {𝑥𝐵𝐶 ∈ V}
85, 7syl6reqr 2872 1 (𝜑 → dom 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  wral 3135  {crab 3139  Vcvv 3492  cmpt 5137  dom cdm 5548
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-opab 5120  df-mpt 5138  df-xp 5554  df-rel 5555  df-cnv 5556  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561
This theorem is referenced by:  lo1eq  14913  rlimeq  14914  rlimcld2  14923  rlimcn2  14935  rlimmptrcl  14952  rlimsqzlem  14993  dprdz  19081  alexsublem  22580  cmetcaulem  23818  minveclem3b  23958  mbfneg  24178  mbfsup  24192  mbfinf  24193  mbflimsup  24194  itg2monolem1  24278  itg2mono  24281  itg2i1fseq2  24284  itg2cnlem1  24289  isibl2  24294  iblcnlem  24316  limccnp2  24417  limcco  24418  dvmptres3  24480  itgsubstlem  24572  iblulm  24922  rlimcnp2  25471  dchrisumlema  25991  htthlem  28621  expgrowth  40544  mptelpm  41308  choicefi  41339  mullimc  41773  limcmptdm  41792  dvsinax  42073  dirkercncflem2  42266  fourierdlem62  42330  psmeasure  42630  ovnovollem2  42816  smflimsuplem2  42972
  Copyright terms: Public domain W3C validator