Theorem dmmptd 6651

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

Step	Hyp	Ref	Expression
1		dmmptd.a	. . 3 ⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶)
2	1	dmmpt 6212	. 2 ⊢ dom 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝐶 ∈ V}
3		dmmptd.c	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉)
4	3	elexd 3467	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ V)
5	4	ralrimiva 3144	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝐶 ∈ V)
6		rabid2 3437	. . 3 ⊢ (𝐵 = {𝑥 ∈ 𝐵 ∣ 𝐶 ∈ V} ↔ ∀𝑥 ∈ 𝐵 𝐶 ∈ V)
7	5, 6	sylibr 236	. 2 ⊢ (𝜑 → 𝐵 = {𝑥 ∈ 𝐵 ∣ 𝐶 ∈ V})
8	2, 7	eqtr4id 2806	1 ⊢ (𝜑 → dom 𝐴 = 𝐵)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1550   ∈ wcel 2132  ∀wral 3066  {crab 3404  Vcvv 3444   ↦ cmpt 5171  dom cdm 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-pr 5380

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ral 3067  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-br 5091  df-opab 5153  df-mpt 5172  df-xp 5642  df-rel 5643  df-cnv 5644  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649

This theorem is referenced by:  lo1eq  15567  rlimeq  15568  rlimcld2  15577  rlimcn3  15589  rlimmptrcl  15607  rlimsqzlem  15648  dprdz  20044  alexsublem  24073  cmetcaulem  25319  minveclem3b  25459  mbfneg  25681  mbfsup  25695  mbfinf  25696  mbflimsup  25697  itg2monolem1  25781  itg2mono  25784  itg2i1fseq2  25787  itg2cnlem1  25792  isibl2  25797  iblcnlem  25820  limccnp2  25923  limcco  25924  dvmptres3  25987  itgsubstlem  26079  iblulm  26436  rlimcnp2  26997  dchrisumlema  27518  htthlem  31055  qusrn  33541  esplyfvaln  33815  extdgfialglem1  33933  algextdeglem4  33961  dmqmap  38890  expgrowth  44849  mptelpm  45692  choicefi  45715  mullimc  46130  limcmptdm  46147  dvsinax  46425  dirkercncflem2  46616  fourierdlem62  46680  psmeasure  46983  ovnovollem2  47169  smfmbfcex  47272  smflimsuplem2  47333