Theorem fmpo 7838

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

Syntax hints:   ↔ wb 209   = wceq 1543   ∈ wcel 2110  ∀wral 3061  {csn 4541  ∪ ciun 4904   × cxp 5549  ⟶wf 6376   ∈ cmpo 7215

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322  ax-un 7523

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-fv 6388  df-oprab 7217  df-mpo 7218  df-1st 7761  df-2nd 7762

This theorem is referenced by:  fnmpo  7839  ovmpoelrn  7842  fmpoco  7863  eroprf  8497  omxpenlem  8746  mapxpen  8812  dffi3  9047  ixpiunwdom  9206  cantnfvalf  9280  iunfictbso  9728  axdc4lem  10069  axcclem  10071  addpqf  10558  mulpqf  10560  subf  11080  xaddf  12814  xmulf  12862  ixxf  12945  ioof  13035  fzf  13099  fzof  13240  axdc4uzlem  13556  sadcf  16012  smupf  16037  gcdf  16071  eucalgf  16140  vdwapf  16525  prdsplusg  16963  prdsmulr  16964  prdsvsca  16965  prdshom  16972  imasvscaf  17044  xpsff1o  17072  wunnat  17463  wunnatOLD  17464  catcoppccl  17623  catcoppcclOLD  17624  catcfuccl  17625  catcfucclOLD  17626  catcxpccl  17714  catcxpcclOLD  17715  evlfcl  17730  hofcl  17767  mgmplusf  18124  grpsubf  18442  subgga  18694  lactghmga  18797  sylow1lem2  18988  sylow3lem1  19016  lsmssv  19032  smndlsmidm  19045  lsmidmOLD  19053  efgmf  19103  efgtf  19112  frgpuptf  19160  lmodscaf  19921  xrsds  20406  phlipf  20614  evlslem2  21039  mamucl  21298  matbas2d  21320  mamumat1cl  21336  ordtbas2  22088  iccordt  22111  txuni2  22462  xkotf  22482  txbasval  22503  tx1stc  22547  xkococn  22557  cnmpt12  22564  cnmpt21  22568  cnmpt2t  22570  cnmpt22  22571  cnmptcom  22575  cnmpt2k  22585  txswaphmeo  22702  xpstopnlem1  22706  cnmpt2plusg  22985  cnmpt2vsca  23092  prdsdsf  23265  blfvalps  23281  blfps  23304  blf  23305  stdbdmet  23414  met2ndci  23420  dscmet  23470  xrsxmet  23706  cnmpt2ds  23740  cnmpopc  23825  iimulcn  23835  ishtpy  23869  reparphti  23894  cnmpt2ip  24145  bcthlem5  24225  rrxmet  24305  dyadf  24488  itg1addlem2  24594  mbfi1fseqlem1  24613  mbfi1fseqlem3  24615  mbfi1fseqlem4  24616  mbfi1fseqlem5  24617  cxpcn3  25634  sgmf  26027  midf  26867  grpodivf  28619  nvmf  28726  ipf  28794  hvsubf  29096  ofoprabco  30721  suppovss  30737  fedgmullem1  31424  fedgmullem2  31425  fedgmul  31426  sitmf  32031  cvxsconn  32918  cvmlift2lem5  32982  uncf  35493  mblfinlem1  35551  mblfinlem2  35552  sdclem1  35638  metf1o  35650  rrnval  35722  rrnmet  35724  resubf  40072  sn-subf  40118  frmx  40438  frmy  40439  mnringmulrcld  41519  icof  42432