Theorem fmpo 7940

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

Syntax hints:   ↔ wb 205   = wceq 1539   ∈ wcel 2104  ∀wral 3062  {csn 4565  ∪ ciun 4931   × cxp 5598  ⟶wf 6454   ∈ cmpo 7309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361  ax-un 7620

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3306  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5500  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-fv 6466  df-oprab 7311  df-mpo 7312  df-1st 7863  df-2nd 7864

This theorem is referenced by:  fnmpo  7941  ovmpoelrn  7944  fmpoco  7967  eroprf  8635  omxpenlem  8898  mapxpen  8968  dffi3  9238  ixpiunwdom  9397  cantnfvalf  9471  iunfictbso  9920  axdc4lem  10261  axcclem  10263  addpqf  10750  mulpqf  10752  subf  11273  xaddf  13008  xmulf  13056  ixxf  13139  ioof  13229  fzf  13293  fzof  13434  axdc4uzlem  13753  sadcf  16209  smupf  16234  gcdf  16268  eucalgf  16337  vdwapf  16722  prdsplusg  17218  prdsmulr  17219  prdsvsca  17220  prdshom  17227  imasvscaf  17299  xpsff1o  17327  wunnat  17721  wunnatOLD  17722  catcoppccl  17881  catcoppcclOLD  17882  catcfuccl  17883  catcfucclOLD  17884  catcxpccl  17973  catcxpcclOLD  17974  evlfcl  17989  hofcl  18026  mgmplusf  18385  grpsubf  18703  subgga  18955  lactghmga  19062  sylow1lem2  19253  sylow3lem1  19281  lsmssv  19297  smndlsmidm  19310  lsmidmOLD  19318  efgmf  19368  efgtf  19377  frgpuptf  19425  lmodscaf  20194  xrsds  20690  phlipf  20906  evlslem2  21338  mamucl  21597  matbas2d  21621  mamumat1cl  21637  ordtbas2  22391  iccordt  22414  txuni2  22765  xkotf  22785  txbasval  22806  tx1stc  22850  xkococn  22860  cnmpt12  22867  cnmpt21  22871  cnmpt2t  22873  cnmpt22  22874  cnmptcom  22878  cnmpt2k  22888  txswaphmeo  23005  xpstopnlem1  23009  cnmpt2plusg  23288  cnmpt2vsca  23395  prdsdsf  23569  blfvalps  23585  blfps  23608  blf  23609  stdbdmet  23721  met2ndci  23727  dscmet  23777  xrsxmet  24021  cnmpt2ds  24055  cnmpopc  24140  iimulcn  24150  ishtpy  24184  reparphti  24209  cnmpt2ip  24461  bcthlem5  24541  rrxmet  24621  dyadf  24804  itg1addlem2  24910  mbfi1fseqlem1  24929  mbfi1fseqlem3  24931  mbfi1fseqlem4  24932  mbfi1fseqlem5  24933  cxpcn3  25950  sgmf  26343  midf  27186  grpodivf  28949  nvmf  29056  ipf  29124  hvsubf  29426  ofoprabco  31050  suppovss  31066  fedgmullem1  31759  fedgmullem2  31760  fedgmul  31761  sitmf  32368  cvxsconn  33254  cvmlift2lem5  33318  uncf  35804  mblfinlem1  35862  mblfinlem2  35863  sdclem1  35949  metf1o  35961  rrnval  36033  rrnmet  36035  resubf  40559  sn-subf  40605  frmx  40931  frmy  40932  ofoafg  41245  naddcnff  41253  mnringmulrcld  42059  icof  42979