Theorem fmpo 8065

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ∀wral 3076  {csn 4584  ∪ ciun 4951   × cxp 5653  ⟶wf 6529   ∈ cmpo 7415

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7736

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-oprab 7417  df-mpo 7418  df-1st 7986  df-2nd 7987

This theorem is used by:  fnmpo  8066  fmpodg  8069  ovmpoelrn  8071  fmpoco  8092  eroprf  8815  uncf  8870  omxpenlem  9076  mapxpen  9141  dffi3  9401  ixpiunwdom  9562  cantnfvalf  9644  iunfictbso  10117  axdc4lem  10457  axcclem  10459  addpqf  10953  mulpqf  10955  subf  11483  xaddf  13276  xmulf  13324  ixxf  13408  ioof  13500  fzf  13565  fzof  13711  axdc4uzlem  14047  sadcf  16543  smupf  16568  gcdf  16602  eucalgf  16673  vdwapf  17064  prdsplusg  17543  prdsmulr  17544  prdsvsca  17545  prdshom  17552  imasvscaf  17625  xpsff1o  17653  wunnat  18048  catcoppccl  18206  catcfuccl  18207  catcxpccl  18295  evlfcl  18310  hofcl  18347  mgmplusf  18740  grpsubf  19142  subgga  19427  lactghmga  19532  sylow1lem2  19726  sylow3lem1  19754  lsmssv  19770  smndlsmidm  19783  efgmf  19840  efgtf  19849  frgpuptf  19897  lmodscaf  21068  xrsds  21623  phlipf  21865  evlslem2  22295  mamucl  22623  matbas2d  22645  mamumat1cl  22661  ordtbas2  23416  iccordt  23439  txuni2  23791  xkotf  23811  txbasval  23832  tx1stc  23876  xkococn  23886  cnmpt12  23893  cnmpt21  23897  cnmpt2t  23899  cnmpt22  23900  cnmptcom  23904  cnmpt2k  23914  txswaphmeo  24031  xpstopnlem1  24035  cnmpt2plusg  24314  cnmpt2vsca  24421  prdsdsf  24593  blfvalps  24609  blfps  24632  blf  24633  stdbdmet  24742  met2ndci  24748  dscmet  24798  xrsxmet  25036  cnmpt2ds  25070  cnmpopc  25156  iimulcn  25166  ishtpy  25200  reparphti  25225  cnmpt2ip  25476  bcthlem5  25556  rrxmet  25636  dyadf  25819  itg1addlem2  25925  mbfi1fseqlem1  25943  mbfi1fseqlem3  25945  mbfi1fseqlem4  25946  mbfi1fseqlem5  25947  cxpcn3  26985  sgmf  27381  subsf  28329  midf  29160  grpodivf  31019  nvmf  31126  ipf  31194  hvsubf  31496  ofoprabco  33137  suppovss  33153  elrgspnlem2  33683  fedgmullem1  34139  fedgmullem2  34140  fedgmul  34141  sitmf  34863  cvxsconn  35822  cvmlift2lem5  35886  mblfinlem1  38406  mblfinlem2  38407  sdclem1  38493  metf1o  38505  rrnval  38577  rrnmet  38579  aks6d1c3  42989  fmpocos  43103  resubf  43256  sn-subf  43304  evlselv  43435  frmx  43754  frmy  43755  ofoafg  44195  naddcnff  44203  mnringmulrcld  45066  icof  46049  rescofuf  50019