Theorem fmpo 7622

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

Syntax hints:   ↔ wb 207   = wceq 1522   ∈ wcel 2081  ∀wral 3105  {csn 4472  ∪ ciun 4825   × cxp 5441  ⟶wf 6221   ∈ cmpo 7018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-iun 4827  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-fv 6233  df-oprab 7020  df-mpo 7021  df-1st 7545  df-2nd 7546

This theorem is referenced by:  fnmpo  7623  ovmpoelrn  7626  fmpoco  7646  eroprf  8245  omxpenlem  8465  mapxpen  8530  dffi3  8741  ixpiunwdom  8901  cantnfvalf  8974  iunfictbso  9386  axdc4lem  9723  axcclem  9725  addpqf  10212  mulpqf  10214  subf  10735  xaddf  12467  xmulf  12515  ixxf  12598  ioof  12685  fzf  12746  fzof  12885  axdc4uzlem  13201  sadcf  15635  smupf  15660  gcdf  15694  eucalgf  15756  vdwapf  16137  prdsval  16557  prdsplusg  16560  prdsmulr  16561  prdsvsca  16562  prdsds  16566  prdshom  16569  imasvscaf  16641  xpsff1o  16669  wunnat  17055  catcoppccl  17197  catcfuccl  17198  catcxpccl  17286  evlfcl  17301  hofcl  17338  plusffval  17686  mgmplusf  17690  grpsubf  17935  subgga  18171  lactghmga  18263  sylow1lem2  18454  sylow3lem1  18482  lsmssv  18498  lsmidm  18517  efgmf  18566  efgtf  18575  frgpuptf  18623  scaffval  19342  lmodscaf  19346  evlslem2  19979  xrsds  20270  ipffval  20474  phlipf  20478  mamucl  20694  matbas2d  20716  mamumat1cl  20732  ordtbas2  21483  iccordt  21506  txuni2  21857  xkotf  21877  txbasval  21898  tx1stc  21942  xkococn  21952  cnmpt12  21959  cnmpt21  21963  cnmpt2t  21965  cnmpt22  21966  cnmptcom  21970  cnmpt2k  21980  txswaphmeo  22097  xpstopnlem1  22101  cnmpt2plusg  22380  cnmpt2vsca  22486  prdsdsf  22660  blfvalps  22676  blfps  22699  blf  22700  stdbdmet  22809  met2ndci  22815  dscmet  22865  xrsxmet  23100  cnmpt2ds  23134  cnmpopc  23215  iimulcn  23225  ishtpy  23259  reparphti  23284  cnmpt2ip  23534  bcthlem5  23614  rrxmet  23694  dyadf  23875  itg1addlem2  23981  mbfi1fseqlem1  23999  mbfi1fseqlem3  24001  mbfi1fseqlem4  24002  mbfi1fseqlem5  24003  cxpcn3  25010  sgmf  25404  midf  26244  grpodivf  28006  nvmf  28113  ipf  28181  hvsubf  28483  ofoprabco  30099  suppovss  30116  fedgmullem1  30629  fedgmullem2  30630  fedgmul  30631  sitmf  31227  cvxsconn  32098  cvmlift2lem5  32162  uncf  34402  mblfinlem1  34460  mblfinlem2  34461  sdclem1  34550  metf1o  34562  rrnval  34637  rrnmet  34639  resubf  38734  frmx  38995  frmy  38996  icof  41022