Theorem fmpo 8064

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

Syntax hints:   ↔ wb 209   = wceq 1567   ∈ wcel 2149  ∀wral 3085  {csn 4594  ∪ ciun 4960   × cxp 5660  ⟶wf 6533   ∈ cmpo 7413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-oprab 7415  df-mpo 7416  df-1st 7985  df-2nd 7986

This theorem is referenced by:  fnmpo  8065  ovmpoelrn  8068  fmpoco  8089  eroprf  8812  omxpenlem  9065  mapxpen  9130  dffi3  9390  ixpiunwdom  9551  cantnfvalf  9633  iunfictbso  10097  axdc4lem  10438  axcclem  10440  addpqf  10928  mulpqf  10930  subf  11458  xaddf  13249  xmulf  13297  ixxf  13381  ioof  13473  fzf  13538  fzof  13683  axdc4uzlem  14018  sadcf  16510  smupf  16535  gcdf  16569  eucalgf  16640  vdwapf  17031  prdsplusg  17510  prdsmulr  17511  prdsvsca  17512  prdshom  17519  imasvscaf  17592  xpsff1o  17620  wunnat  18015  catcoppccl  18173  catcfuccl  18174  catcxpccl  18262  evlfcl  18277  hofcl  18314  mgmplusf  18707  grpsubf  19084  subgga  19369  lactghmga  19474  sylow1lem2  19668  sylow3lem1  19696  lsmssv  19712  smndlsmidm  19725  efgmf  19782  efgtf  19791  frgpuptf  19839  lmodscaf  20982  xrsds  21528  phlipf  21770  evlslem2  22198  mamucl  22526  matbas2d  22548  mamumat1cl  22564  ordtbas2  23316  iccordt  23339  txuni2  23690  xkotf  23710  txbasval  23731  tx1stc  23775  xkococn  23785  cnmpt12  23792  cnmpt21  23796  cnmpt2t  23798  cnmpt22  23799  cnmptcom  23803  cnmpt2k  23813  txswaphmeo  23930  xpstopnlem1  23934  cnmpt2plusg  24213  cnmpt2vsca  24320  prdsdsf  24492  blfvalps  24508  blfps  24531  blf  24532  stdbdmet  24641  met2ndci  24647  dscmet  24697  xrsxmet  24935  cnmpt2ds  24969  cnmpopc  25055  iimulcn  25065  ishtpy  25099  reparphti  25124  cnmpt2ip  25375  bcthlem5  25455  rrxmet  25535  dyadf  25718  itg1addlem2  25824  mbfi1fseqlem1  25842  mbfi1fseqlem3  25844  mbfi1fseqlem4  25845  mbfi1fseqlem5  25846  cxpcn3  26878  sgmf  27274  subsf  28222  midf  29042  grpodivf  30830  nvmf  30937  ipf  31005  hvsubf  31307  ofoprabco  32949  suppovss  32966  elrgspnlem2  33503  fedgmullem1  33963  fedgmullem2  33964  fedgmul  33965  sitmf  34686  cvxsconn  35633  cvmlift2lem5  35697  uncf  38137  mblfinlem1  38195  mblfinlem2  38196  sdclem1  38281  metf1o  38293  rrnval  38365  rrnmet  38367  aks6d1c3  42779  fmpocos  42893  resubf  43031  sn-subf  43079  evlselv  43212  frmx  43531  frmy  43532  ofoafg  43972  naddcnff  43980  mnringmulrcld  44843  icof  45826  fmpodg  49531  rescofuf  49755