Theorem dmmptd 6643

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 6204	. 2 ⊢ dom 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝐶 ∈ V}
3		dmmptd.c	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉)
4	3	elexd 3453	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ V)
5	4	ralrimiva 3129	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝐶 ∈ V)
6		rabid2 3422	. . 3 ⊢ (𝐵 = {𝑥 ∈ 𝐵 ∣ 𝐶 ∈ V} ↔ ∀𝑥 ∈ 𝐵 𝐶 ∈ V)
7	5, 6	sylibr 234	. 2 ⊢ (𝜑 → 𝐵 = {𝑥 ∈ 𝐵 ∣ 𝐶 ∈ V})
8	2, 7	eqtr4id 2790	1 ⊢ (𝜑 → dom 𝐴 = 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3051  {crab 3389  Vcvv 3429   ↦ cmpt 5166  dom cdm 5631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-mpt 5167  df-xp 5637  df-rel 5638  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644

This theorem is referenced by:  lo1eq  15530  rlimeq  15531  rlimcld2  15540  rlimcn3  15552  rlimmptrcl  15570  rlimsqzlem  15611  dprdz  20007  alexsublem  24009  cmetcaulem  25255  minveclem3b  25395  mbfneg  25617  mbfsup  25631  mbfinf  25632  mbflimsup  25633  itg2monolem1  25717  itg2mono  25720  itg2i1fseq2  25723  itg2cnlem1  25728  isibl2  25733  iblcnlem  25756  limccnp2  25859  limcco  25860  dvmptres3  25923  itgsubstlem  26015  iblulm  26372  rlimcnp2  26930  dchrisumlema  27451  htthlem  30988  qusrn  33469  esplyfvaln  33718  extdgfialglem1  33836  algextdeglem4  33864  dmqmap  38774  expgrowth  44762  mptelpm  45606  choicefi  45629  mullimc  46046  limcmptdm  46063  dvsinax  46341  dirkercncflem2  46532  fourierdlem62  46596  psmeasure  46899  ovnovollem2  47085  smfmbfcex  47188  smflimsuplem2  47249