Theorem dmmpo 7766

Description: Domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.)

Hypotheses

Ref	Expression
fmpo.1	⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
fnmpoi.2	⊢ 𝐶 ∈ V

Assertion

Ref	Expression
dmmpo	⊢ dom 𝐹 = (𝐴 × 𝐵)

Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦

Allowed substitution hints:   𝐶(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem dmmpo

Step	Hyp	Ref	Expression
1		fmpo.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
2		fnmpoi.2	. . 3 ⊢ 𝐶 ∈ V
3	1, 2	fnmpoi 7765	. 2 ⊢ 𝐹 Fn (𝐴 × 𝐵)
4		fndm 6452	. 2 ⊢ (𝐹 Fn (𝐴 × 𝐵) → dom 𝐹 = (𝐴 × 𝐵))
5	3, 4	ax-mp 5	1 ⊢ dom 𝐹 = (𝐴 × 𝐵)

Syntax hints:   = wceq 1536   ∈ wcel 2113  Vcvv 3493   × cxp 5550  dom cdm 5552   Fn wfn 6347   ∈ cmpo 7155

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5327  ax-un 7458

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-ne 3016  df-ral 3142  df-rex 3143  df-rab 3146  df-v 3495  df-sbc 3771  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4465  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4836  df-iun 4918  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5457  df-xp 5558  df-rel 5559  df-cnv 5560  df-co 5561  df-dm 5562  df-rn 5563  df-res 5564  df-ima 5565  df-iota 6311  df-fun 6354  df-fn 6355  df-f 6356  df-fv 6360  df-oprab 7157  df-mpo 7158  df-1st 7686  df-2nd 7687

This theorem is referenced by:  1div0  11296  swrd00  14002  swrd0  14016  pfx00  14032  pfx0  14033  repsundef  14129  cshnz  14150  imasvscafn  16806  imasvscaval  16807  iscnp2  21843  xkococnlem  22263  ucnima  22886  ucnprima  22887  tngtopn  23255  1div0apr  28245  smatlem  31086  elunirnmbfm  31535  rrxsphere  44809