Theorem fmpo 8049

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

Syntax hints:   ↔ wb 208   = wceq 1560   ∈ wcel 2142  ∀wral 3076  {csn 4582  ∪ ciun 4949   × cxp 5645  ⟶wf 6517   ∈ cmpo 7398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-fv 6529  df-oprab 7400  df-mpo 7401  df-1st 7970  df-2nd 7971

This theorem is referenced by:  fnmpo  8050  ovmpoelrn  8053  fmpoco  8074  eroprf  8797  omxpenlem  9050  mapxpen  9115  dffi3  9377  ixpiunwdom  9538  cantnfvalf  9620  iunfictbso  10070  axdc4lem  10412  axcclem  10414  addpqf  10902  mulpqf  10904  subf  11432  xaddf  13227  xmulf  13275  ixxf  13359  ioof  13451  fzf  13516  fzof  13661  axdc4uzlem  13996  sadcf  16487  smupf  16512  gcdf  16546  eucalgf  16617  vdwapf  17008  prdsplusg  17487  prdsmulr  17488  prdsvsca  17489  prdshom  17496  imasvscaf  17569  xpsff1o  17597  wunnat  17992  catcoppccl  18150  catcfuccl  18151  catcxpccl  18239  evlfcl  18254  hofcl  18291  mgmplusf  18684  grpsubf  19061  subgga  19340  lactghmga  19445  sylow1lem2  19639  sylow3lem1  19667  lsmssv  19683  smndlsmidm  19696  efgmf  19753  efgtf  19762  frgpuptf  19810  lmodscaf  20948  xrsds  21459  phlipf  21701  evlslem2  22129  mamucl  22458  matbas2d  22480  mamumat1cl  22496  ordtbas2  23248  iccordt  23271  txuni2  23622  xkotf  23642  txbasval  23663  tx1stc  23707  xkococn  23717  cnmpt12  23724  cnmpt21  23728  cnmpt2t  23730  cnmpt22  23731  cnmptcom  23735  cnmpt2k  23745  txswaphmeo  23862  xpstopnlem1  23866  cnmpt2plusg  24145  cnmpt2vsca  24252  prdsdsf  24424  blfvalps  24440  blfps  24463  blf  24464  stdbdmet  24573  met2ndci  24579  dscmet  24629  xrsxmet  24867  cnmpt2ds  24901  cnmpopc  24987  iimulcn  24997  ishtpy  25031  reparphti  25056  cnmpt2ip  25307  bcthlem5  25387  rrxmet  25467  dyadf  25650  itg1addlem2  25756  mbfi1fseqlem1  25774  mbfi1fseqlem3  25776  mbfi1fseqlem4  25777  mbfi1fseqlem5  25778  cxpcn3  26810  sgmf  27206  subsf  28154  midf  28946  grpodivf  30738  nvmf  30845  ipf  30913  hvsubf  31215  ofoprabco  32863  suppovss  32880  elrgspnlem2  33421  fedgmullem1  33923  fedgmullem2  33924  fedgmul  33925  sitmf  34646  cvxsconn  35590  cvmlift2lem5  35654  uncf  38095  mblfinlem1  38153  mblfinlem2  38154  sdclem1  38239  metf1o  38251  rrnval  38323  rrnmet  38325  aks6d1c3  42737  fmpocos  42849  resubf  42987  sn-subf  43035  evlselv  43168  frmx  43487  frmy  43488  ofoafg  43928  naddcnff  43936  mnringmulrcld  44801  icof  45792  fmpodg  49487  rescofuf  49711