Theorem fmpo 8012

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∀wral 3051  {csn 4580  ∪ ciun 4946   × cxp 5622  ⟶wf 6488   ∈ cmpo 7360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-oprab 7362  df-mpo 7363  df-1st 7933  df-2nd 7934

This theorem is referenced by:  fnmpo  8013  ovmpoelrn  8016  fmpoco  8037  eroprf  8752  omxpenlem  9006  mapxpen  9071  dffi3  9334  ixpiunwdom  9495  cantnfvalf  9574  iunfictbso  10024  axdc4lem  10365  axcclem  10367  addpqf  10855  mulpqf  10857  subf  11382  xaddf  13139  xmulf  13187  ixxf  13271  ioof  13363  fzf  13427  fzof  13572  axdc4uzlem  13906  sadcf  16380  smupf  16405  gcdf  16439  eucalgf  16510  vdwapf  16900  prdsplusg  17378  prdsmulr  17379  prdsvsca  17380  prdshom  17387  imasvscaf  17460  xpsff1o  17488  wunnat  17883  catcoppccl  18041  catcfuccl  18042  catcxpccl  18130  evlfcl  18145  hofcl  18182  mgmplusf  18575  grpsubf  18949  subgga  19229  lactghmga  19334  sylow1lem2  19528  sylow3lem1  19556  lsmssv  19572  smndlsmidm  19585  efgmf  19642  efgtf  19651  frgpuptf  19699  lmodscaf  20835  xrsds  21364  phlipf  21607  evlslem2  22034  mamucl  22345  matbas2d  22367  mamumat1cl  22383  ordtbas2  23135  iccordt  23158  txuni2  23509  xkotf  23529  txbasval  23550  tx1stc  23594  xkococn  23604  cnmpt12  23611  cnmpt21  23615  cnmpt2t  23617  cnmpt22  23618  cnmptcom  23622  cnmpt2k  23632  txswaphmeo  23749  xpstopnlem1  23753  cnmpt2plusg  24032  cnmpt2vsca  24139  prdsdsf  24311  blfvalps  24327  blfps  24350  blf  24351  stdbdmet  24460  met2ndci  24466  dscmet  24516  xrsxmet  24754  cnmpt2ds  24788  cnmpopc  24878  iimulcn  24890  iimulcnOLD  24891  ishtpy  24927  reparphti  24952  reparphtiOLD  24953  cnmpt2ip  25204  bcthlem5  25284  rrxmet  25364  dyadf  25548  itg1addlem2  25654  mbfi1fseqlem1  25672  mbfi1fseqlem3  25674  mbfi1fseqlem4  25675  mbfi1fseqlem5  25676  cxpcn3  26714  sgmf  27111  subsf  28060  midf  28848  grpodivf  30613  nvmf  30720  ipf  30788  hvsubf  31090  ofoprabco  32742  suppovss  32760  elrgspnlem2  33325  fedgmullem1  33786  fedgmullem2  33787  fedgmul  33788  sitmf  34509  cvxsconn  35437  cvmlift2lem5  35501  uncf  37800  mblfinlem1  37858  mblfinlem2  37859  sdclem1  37944  metf1o  37956  rrnval  38028  rrnmet  38030  aks6d1c3  42377  fmpocos  42490  resubf  42636  sn-subf  42684  evlselv  42830  frmx  43155  frmy  43156  ofoafg  43596  naddcnff  43604  mnringmulrcld  44469  icof  45463  fmpodg  49114  rescofuf  49338