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

Theorem dmmptd 5919
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 3180 . . . . 5 (𝐶𝑉𝐶 ∈ V)
31, 2syl 17 . . . 4 ((𝜑𝑥𝐵) → 𝐶 ∈ V)
43ralrimiva 2944 . . 3 (𝜑 → ∀𝑥𝐵 𝐶 ∈ V)
5 rabid2 3091 . . 3 (𝐵 = {𝑥𝐵𝐶 ∈ V} ↔ ∀𝑥𝐵 𝐶 ∈ V)
64, 5sylibr 222 . 2 (𝜑𝐵 = {𝑥𝐵𝐶 ∈ V})
7 dmmptd.a . . 3 𝐴 = (𝑥𝐵𝐶)
87dmmpt 5529 . 2 dom 𝐴 = {𝑥𝐵𝐶 ∈ V}
96, 8syl6reqr 2658 1 (𝜑 → dom 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1975  wral 2891  {crab 2895  Vcvv 3168  cmpt 4633  dom cdm 5024
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pr 4824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ral 2896  df-rex 2897  df-rab 2900  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-br 4574  df-opab 4634  df-mpt 4635  df-xp 5030  df-rel 5031  df-cnv 5032  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037
This theorem is referenced by:  cantnfp1lem2  8432  lo1eq  14089  rlimeq  14090  rlimcld2  14099  rlimcn2  14111  rlimmptrcl  14128  rlimsqzlem  14169  dprdz  18194  alexsublem  21596  cmetcaulem  22808  minveclem3b  22920  mbfneg  23136  mbfsup  23150  mbfinf  23151  mbflimsup  23152  itg2monolem1  23236  itg2mono  23239  itg2i1fseq2  23242  itg2cnlem1  23247  isibl2  23252  iblcnlem  23274  limccnp2  23375  limcco  23376  dvmptres3  23438  itgsubstlem  23528  iblulm  23878  rlimcnp2  24406  dchrisumlema  24890  htthlem  26960  expgrowth  37355  mptelpm  38151  choicefi  38186  mullimc  38483  limcmptdm  38502  dvsinax  38601  dirkercncflem2  38797  fourierdlem62  38861  psmeasure  39164  ovnovollem2  39347
  Copyright terms: Public domain W3C validator