Theorem fmpo 8015

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∀wral 3052  {csn 4568  ∪ ciun 4934   × cxp 5623  ⟶wf 6489   ∈ cmpo 7363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371  ax-un 7683

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-oprab 7365  df-mpo 7366  df-1st 7936  df-2nd 7937

This theorem is referenced by:  fnmpo  8016  ovmpoelrn  8019  fmpoco  8039  eroprf  8756  omxpenlem  9010  mapxpen  9075  dffi3  9338  ixpiunwdom  9499  cantnfvalf  9580  iunfictbso  10030  axdc4lem  10371  axcclem  10373  addpqf  10861  mulpqf  10863  subf  11389  xaddf  13170  xmulf  13218  ixxf  13302  ioof  13394  fzf  13459  fzof  13604  axdc4uzlem  13939  sadcf  16416  smupf  16441  gcdf  16475  eucalgf  16546  vdwapf  16937  prdsplusg  17415  prdsmulr  17416  prdsvsca  17417  prdshom  17424  imasvscaf  17497  xpsff1o  17525  wunnat  17920  catcoppccl  18078  catcfuccl  18079  catcxpccl  18167  evlfcl  18182  hofcl  18219  mgmplusf  18612  grpsubf  18989  subgga  19269  lactghmga  19374  sylow1lem2  19568  sylow3lem1  19596  lsmssv  19612  smndlsmidm  19625  efgmf  19682  efgtf  19691  frgpuptf  19739  lmodscaf  20873  xrsds  21402  phlipf  21645  evlslem2  22070  mamucl  22379  matbas2d  22401  mamumat1cl  22417  ordtbas2  23169  iccordt  23192  txuni2  23543  xkotf  23563  txbasval  23584  tx1stc  23628  xkococn  23638  cnmpt12  23645  cnmpt21  23649  cnmpt2t  23651  cnmpt22  23652  cnmptcom  23656  cnmpt2k  23666  txswaphmeo  23783  xpstopnlem1  23787  cnmpt2plusg  24066  cnmpt2vsca  24173  prdsdsf  24345  blfvalps  24361  blfps  24384  blf  24385  stdbdmet  24494  met2ndci  24500  dscmet  24550  xrsxmet  24788  cnmpt2ds  24822  cnmpopc  24908  iimulcn  24918  ishtpy  24952  reparphti  24977  cnmpt2ip  25228  bcthlem5  25308  rrxmet  25388  dyadf  25571  itg1addlem2  25677  mbfi1fseqlem1  25695  mbfi1fseqlem3  25697  mbfi1fseqlem4  25698  mbfi1fseqlem5  25699  cxpcn3  26728  sgmf  27125  subsf  28073  midf  28861  grpodivf  30627  nvmf  30734  ipf  30802  hvsubf  31104  ofoprabco  32755  suppovss  32772  elrgspnlem2  33322  fedgmullem1  33792  fedgmullem2  33793  fedgmul  33794  sitmf  34515  cvxsconn  35444  cvmlift2lem5  35508  uncf  37937  mblfinlem1  37995  mblfinlem2  37996  sdclem1  38081  metf1o  38093  rrnval  38165  rrnmet  38167  aks6d1c3  42579  fmpocos  42692  resubf  42830  sn-subf  42878  evlselv  43037  frmx  43362  frmy  43363  ofoafg  43803  naddcnff  43811  mnringmulrcld  44676  icof  45669  fmpodg  49359  rescofuf  49583