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

Theorem dmmptd 6713
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.a . . 3 𝐴 = (𝑥𝐵𝐶)
21dmmpt 6261 . 2 dom 𝐴 = {𝑥𝐵𝐶 ∈ V}
3 dmmptd.c . . . . 5 ((𝜑𝑥𝐵) → 𝐶𝑉)
43elexd 3501 . . . 4 ((𝜑𝑥𝐵) → 𝐶 ∈ V)
54ralrimiva 3143 . . 3 (𝜑 → ∀𝑥𝐵 𝐶 ∈ V)
6 rabid2 3467 . . 3 (𝐵 = {𝑥𝐵𝐶 ∈ V} ↔ ∀𝑥𝐵 𝐶 ∈ V)
75, 6sylibr 234 . 2 (𝜑𝐵 = {𝑥𝐵𝐶 ∈ V})
82, 7eqtr4id 2793 1 (𝜑 → dom 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1536  wcel 2105  wral 3058  {crab 3432  Vcvv 3477  cmpt 5230  dom cdm 5688
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-mpt 5231  df-xp 5694  df-rel 5695  df-cnv 5696  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701
This theorem is referenced by:  lo1eq  15600  rlimeq  15601  rlimcld2  15610  rlimcn3  15622  rlimmptrcl  15640  rlimsqzlem  15681  dprdz  20064  alexsublem  24067  cmetcaulem  25335  minveclem3b  25475  mbfneg  25698  mbfsup  25712  mbfinf  25713  mbflimsup  25714  itg2monolem1  25799  itg2mono  25802  itg2i1fseq2  25805  itg2cnlem1  25810  isibl2  25815  iblcnlem  25838  limccnp2  25941  limcco  25942  dvmptres3  26008  itgsubstlem  26103  iblulm  26464  rlimcnp2  27023  dchrisumlema  27546  htthlem  30945  qusrn  33416  algextdeglem4  33725  expgrowth  44330  mptelpm  45118  choicefi  45142  mullimc  45571  limcmptdm  45590  dvsinax  45868  dirkercncflem2  46059  fourierdlem62  46123  psmeasure  46426  ovnovollem2  46612  smfmbfcex  46715  smflimsuplem2  46776
  Copyright terms: Public domain W3C validator