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 5691	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵)
4	3	feq2i 6647	. 2 ⊢ (𝐹:∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⟶𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷)
5	2, 4	bitri 276	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹:(𝐴 × 𝐵)⟶𝐷)

Syntax hints:   ↔ wb 207   = wceq 1547   ∈ wcel 2119  ∀wral 3053  {csn 4555  ∪ ciun 4921   × cxp 5616  ⟶wf 6481   ∈ cmpo 7358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-fv 6493  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932

This theorem is referenced by:  fnmpo  8011  ovmpoelrn  8014  fmpoco  8034  eroprf  8752  omxpenlem  9006  mapxpen  9071  dffi3  9334  ixpiunwdom  9495  cantnfvalf  9577  iunfictbso  10027  axdc4lem  10368  axcclem  10370  addpqf  10858  mulpqf  10860  subf  11386  xaddf  13167  xmulf  13215  ixxf  13299  ioof  13391  fzf  13456  fzof  13601  axdc4uzlem  13936  sadcf  16413  smupf  16438  gcdf  16472  eucalgf  16543  vdwapf  16934  prdsplusg  17412  prdsmulr  17413  prdsvsca  17414  prdshom  17421  imasvscaf  17494  xpsff1o  17522  wunnat  17917  catcoppccl  18075  catcfuccl  18076  catcxpccl  18164  evlfcl  18179  hofcl  18216  mgmplusf  18609  grpsubf  18986  subgga  19266  lactghmga  19371  sylow1lem2  19565  sylow3lem1  19593  lsmssv  19609  smndlsmidm  19622  efgmf  19679  efgtf  19688  frgpuptf  19736  lmodscaf  20874  xrsds  21385  phlipf  21627  evlslem2  22055  mamucl  22384  matbas2d  22406  mamumat1cl  22422  ordtbas2  23174  iccordt  23197  txuni2  23548  xkotf  23568  txbasval  23589  tx1stc  23633  xkococn  23643  cnmpt12  23650  cnmpt21  23654  cnmpt2t  23656  cnmpt22  23657  cnmptcom  23661  cnmpt2k  23671  txswaphmeo  23788  xpstopnlem1  23792  cnmpt2plusg  24071  cnmpt2vsca  24178  prdsdsf  24350  blfvalps  24366  blfps  24389  blf  24390  stdbdmet  24499  met2ndci  24505  dscmet  24555  xrsxmet  24793  cnmpt2ds  24827  cnmpopc  24913  iimulcn  24923  ishtpy  24957  reparphti  24982  cnmpt2ip  25233  bcthlem5  25313  rrxmet  25393  dyadf  25576  itg1addlem2  25682  mbfi1fseqlem1  25700  mbfi1fseqlem3  25702  mbfi1fseqlem4  25703  mbfi1fseqlem5  25704  cxpcn3  26730  sgmf  27126  subsf  28074  midf  28862  grpodivf  30627  nvmf  30734  ipf  30802  hvsubf  31104  ofoprabco  32756  suppovss  32773  elrgspnlem2  33324  fedgmullem1  33813  fedgmullem2  33814  fedgmul  33815  sitmf  34536  cvxsconn  35471  cvmlift2lem5  35535  uncf  37966  mblfinlem1  38024  mblfinlem2  38025  sdclem1  38110  metf1o  38122  rrnval  38194  rrnmet  38196  aks6d1c3  42608  fmpocos  42720  resubf  42858  sn-subf  42906  evlselv  43039  frmx  43358  frmy  43359  ofoafg  43799  naddcnff  43807  mnringmulrcld  44672  icof  45664  fmpodg  49359  rescofuf  49583