Theorem dmmptd 6493

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.c	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉)
2	1	elexd 3514	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ V)
3	2	ralrimiva 3182	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝐶 ∈ V)
4		rabid2 3381	. . 3 ⊢ (𝐵 = {𝑥 ∈ 𝐵 ∣ 𝐶 ∈ V} ↔ ∀𝑥 ∈ 𝐵 𝐶 ∈ V)
5	3, 4	sylibr 236	. 2 ⊢ (𝜑 → 𝐵 = {𝑥 ∈ 𝐵 ∣ 𝐶 ∈ V})
6		dmmptd.a	. . 3 ⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶)
7	6	dmmpt 6094	. 2 ⊢ dom 𝐴 = {𝑥 ∈ 𝐵 ∣ 𝐶 ∈ V}
8	5, 7	syl6reqr 2875	1 ⊢ (𝜑 → dom 𝐴 = 𝐵)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3138  {crab 3142  Vcvv 3494   ↦ cmpt 5146  dom cdm 5555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-mpt 5147  df-xp 5561  df-rel 5562  df-cnv 5563  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568

This theorem is referenced by:  lo1eq  14925  rlimeq  14926  rlimcld2  14935  rlimcn2  14947  rlimmptrcl  14964  rlimsqzlem  15005  dprdz  19152  alexsublem  22652  cmetcaulem  23891  minveclem3b  24031  mbfneg  24251  mbfsup  24265  mbfinf  24266  mbflimsup  24267  itg2monolem1  24351  itg2mono  24354  itg2i1fseq2  24357  itg2cnlem1  24362  isibl2  24367  iblcnlem  24389  limccnp2  24490  limcco  24491  dvmptres3  24553  itgsubstlem  24645  iblulm  24995  rlimcnp2  25544  dchrisumlema  26064  htthlem  28694  expgrowth  40687  mptelpm  41452  choicefi  41483  mullimc  41917  limcmptdm  41936  dvsinax  42217  dirkercncflem2  42409  fourierdlem62  42473  psmeasure  42773  ovnovollem2  42959  smflimsuplem2  43115