Theorem dmmptd 6681

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 6242	. 2 ⊢ dom 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝐶 ∈ V}
3		dmmptd.c	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉)
4	3	elexd 3486	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ V)
5	4	ralrimiva 3163	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝐶 ∈ V)
6		rabid2 3456	. . 3 ⊢ (𝐵 = {𝑥 ∈ 𝐵 ∣ 𝐶 ∈ V} ↔ ∀𝑥 ∈ 𝐵 𝐶 ∈ V)
7	5, 6	sylibr 237	. 2 ⊢ (𝜑 → 𝐵 = {𝑥 ∈ 𝐵 ∣ 𝐶 ∈ V})
8	2, 7	eqtr4id 2823	1 ⊢ (𝜑 → dom 𝐴 = 𝐵)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∀wral 3085  {crab 3423  Vcvv 3463   ↦ cmpt 5196  dom cdm 5662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-mpt 5197  df-xp 5668  df-rel 5669  df-cnv 5670  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675

This theorem is referenced by:  lo1eq  15618  rlimeq  15619  rlimcld2  15628  rlimcn3  15640  rlimmptrcl  15658  rlimsqzlem  15699  dprdz  20101  alexsublem  24169  cmetcaulem  25415  minveclem3b  25555  mbfneg  25777  mbfsup  25791  mbfinf  25792  mbflimsup  25793  itg2monolem1  25877  itg2mono  25880  itg2i1fseq2  25883  itg2cnlem1  25888  isibl2  25893  iblcnlem  25916  limccnp2  26019  limcco  26020  dvmptres3  26083  itgsubstlem  26175  iblulm  26535  rlimcnp2  27096  dchrisumlema  27617  htthlem  31209  qusrn  33661  esplyfvaln  33908  extdgfialglem1  34026  algextdeglem4  34054  dmqmap  38991  expgrowth  44936  mptelpm  45785  choicefi  45808  mullimc  46223  limcmptdm  46240  dvsinax  46518  dirkercncflem2  46709  fourierdlem62  46773  psmeasure  47076  ovnovollem2  47262  smfmbfcex  47365  smflimsuplem2  47426