Theorem fmpo 8010

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

Hypothesis

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

Assertion

Ref	Expression
fmpo	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷)

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

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

Proof of Theorem fmpo

Step	Hyp	Ref	Expression
1		fmpo.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
2	1	fmpox 8009	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷)
3		iunxpconst 5695	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵)
4	3	feq2i 6652	. 2 ⊢ (𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷)
5	2, 4	bitri 275	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷)

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∀wral 3049  {csn 4578  ∪ ciun 4944   × cxp 5620  ⟶wf 6486   ∈ cmpo 7358

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-fv 6498  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932

This theorem is referenced by:  fnmpo  8011  ovmpoelrn  8014  fmpoco  8035  eroprf  8750  omxpenlem  9004  mapxpen  9069  dffi3  9332  ixpiunwdom  9493  cantnfvalf  9572  iunfictbso  10022  axdc4lem  10363  axcclem  10365  addpqf  10853  mulpqf  10855  subf  11380  xaddf  13137  xmulf  13185  ixxf  13269  ioof  13361  fzf  13425  fzof  13570  axdc4uzlem  13904  sadcf  16378  smupf  16403  gcdf  16437  eucalgf  16508  vdwapf  16898  prdsplusg  17376  prdsmulr  17377  prdsvsca  17378  prdshom  17385  imasvscaf  17458  xpsff1o  17486  wunnat  17881  catcoppccl  18039  catcfuccl  18040  catcxpccl  18128  evlfcl  18143  hofcl  18180  mgmplusf  18573  grpsubf  18947  subgga  19227  lactghmga  19332  sylow1lem2  19526  sylow3lem1  19554  lsmssv  19570  smndlsmidm  19583  efgmf  19640  efgtf  19649  frgpuptf  19697  lmodscaf  20833  xrsds  21362  phlipf  21605  evlslem2  22032  mamucl  22343  matbas2d  22365  mamumat1cl  22381  ordtbas2  23133  iccordt  23156  txuni2  23507  xkotf  23527  txbasval  23548  tx1stc  23592  xkococn  23602  cnmpt12  23609  cnmpt21  23613  cnmpt2t  23615  cnmpt22  23616  cnmptcom  23620  cnmpt2k  23630  txswaphmeo  23747  xpstopnlem1  23751  cnmpt2plusg  24030  cnmpt2vsca  24137  prdsdsf  24309  blfvalps  24325  blfps  24348  blf  24349  stdbdmet  24458  met2ndci  24464  dscmet  24514  xrsxmet  24752  cnmpt2ds  24786  cnmpopc  24876  iimulcn  24888  iimulcnOLD  24889  ishtpy  24925  reparphti  24950  reparphtiOLD  24951  cnmpt2ip  25202  bcthlem5  25282  rrxmet  25362  dyadf  25546  itg1addlem2  25652  mbfi1fseqlem1  25670  mbfi1fseqlem3  25672  mbfi1fseqlem4  25673  mbfi1fseqlem5  25674  cxpcn3  26712  sgmf  27109  subsf  28033  midf  28797  grpodivf  30562  nvmf  30669  ipf  30737  hvsubf  31039  ofoprabco  32691  suppovss  32709  elrgspnlem2  33274  fedgmullem1  33735  fedgmullem2  33736  fedgmul  33737  sitmf  34458  cvxsconn  35386  cvmlift2lem5  35450  uncf  37739  mblfinlem1  37797  mblfinlem2  37798  sdclem1  37883  metf1o  37895  rrnval  37967  rrnmet  37969  aks6d1c3  42316  fmpocos  42432  resubf  42578  sn-subf  42626  evlselv  42772  frmx  43097  frmy  43098  ofoafg  43538  naddcnff  43546  mnringmulrcld  44411  icof  45405  fmpodg  49056  rescofuf  49280