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

Theorem dmmptd 5991
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 ((𝜑𝑥𝐵) → 𝐶𝑉)
2 elex 3202 . . . . 5 (𝐶𝑉𝐶 ∈ V)
31, 2syl 17 . . . 4 ((𝜑𝑥𝐵) → 𝐶 ∈ V)
43ralrimiva 2962 . . 3 (𝜑 → ∀𝑥𝐵 𝐶 ∈ V)
5 rabid2 3111 . . 3 (𝐵 = {𝑥𝐵𝐶 ∈ V} ↔ ∀𝑥𝐵 𝐶 ∈ V)
64, 5sylibr 224 . 2 (𝜑𝐵 = {𝑥𝐵𝐶 ∈ V})
7 dmmptd.a . . 3 𝐴 = (𝑥𝐵𝐶)
87dmmpt 5599 . 2 dom 𝐴 = {𝑥𝐵𝐶 ∈ V}
96, 8syl6reqr 2674 1 (𝜑 → dom 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wcel 1987  wral 2908  {crab 2912  Vcvv 3190  cmpt 4683  dom cdm 5084
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pr 4877
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-br 4624  df-opab 4684  df-mpt 4685  df-xp 5090  df-rel 5091  df-cnv 5092  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097
This theorem is referenced by:  cantnfp1lem2  8536  lo1eq  14249  rlimeq  14250  rlimcld2  14259  rlimcn2  14271  rlimmptrcl  14288  rlimsqzlem  14329  dprdz  18369  alexsublem  21788  cmetcaulem  23026  minveclem3b  23139  mbfneg  23357  mbfsup  23371  mbfinf  23372  mbflimsup  23373  itg2monolem1  23457  itg2mono  23460  itg2i1fseq2  23463  itg2cnlem1  23468  isibl2  23473  iblcnlem  23495  limccnp2  23596  limcco  23597  dvmptres3  23659  itgsubstlem  23749  iblulm  24099  rlimcnp2  24627  dchrisumlema  25111  htthlem  27662  expgrowth  38055  mptelpm  38866  choicefi  38901  mullimc  39284  limcmptdm  39303  dvsinax  39463  dirkercncflem2  39658  fourierdlem62  39722  psmeasure  40025  ovnovollem2  40208  smflimsuplem2  40364
  Copyright terms: Public domain W3C validator