Theorem dmmptd 6678

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3076  {crab 3412  Vcvv 3450   ↦ cmpt 5186  dom cdm 5655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-mpt 5187  df-xp 5661  df-rel 5662  df-cnv 5663  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668

This theorem is used by:  lo1eq  15656  rlimeq  15657  rlimcld2  15666  rlimcn3  15678  rlimmptrcl  15696  rlimsqzlem  15737  dprdz  20160  alexsublem  24271  cmetcaulem  25517  minveclem3b  25657  mbfneg  25879  mbfsup  25893  mbfinf  25894  mbflimsup  25895  itg2monolem1  25979  itg2mono  25982  itg2i1fseq2  25985  itg2cnlem1  25990  isibl2  25995  iblcnlem  26017  limccnp2  26120  limcco  26121  dvmptres3  26184  itgsubstlem  26276  iblulm  26644  rlimcnp2  27204  dchrisumlema  27725  htthlem  31399  qusrn  33839  esplyfvaln  34085  extdgfialglem1  34203  algextdeglem4  34231  dmqmap  39202  expgrowth  45160  mptelpm  46009  choicefi  46032  mullimc  46447  limcmptdm  46464  dvsinax  46742  dirkercncflem2  46933  fourierdlem62  46997  psmeasure  47300  ovnovollem2  47486  smfmbfcex  47589  smflimsuplem2  47650