Theorem fmpo 8021

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∀wral 3051  {csn 4567  ∪ ciun 4933   × cxp 5629  ⟶wf 6494   ∈ cmpo 7369

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506  df-oprab 7371  df-mpo 7372  df-1st 7942  df-2nd 7943

This theorem is referenced by:  fnmpo  8022  ovmpoelrn  8025  fmpoco  8045  eroprf  8762  omxpenlem  9016  mapxpen  9081  dffi3  9344  ixpiunwdom  9505  cantnfvalf  9586  iunfictbso  10036  axdc4lem  10377  axcclem  10379  addpqf  10867  mulpqf  10869  subf  11395  xaddf  13176  xmulf  13224  ixxf  13308  ioof  13400  fzf  13465  fzof  13610  axdc4uzlem  13945  sadcf  16422  smupf  16447  gcdf  16481  eucalgf  16552  vdwapf  16943  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  prdshom  17430  imasvscaf  17503  xpsff1o  17531  wunnat  17926  catcoppccl  18084  catcfuccl  18085  catcxpccl  18173  evlfcl  18188  hofcl  18225  mgmplusf  18618  grpsubf  18995  subgga  19275  lactghmga  19380  sylow1lem2  19574  sylow3lem1  19602  lsmssv  19618  smndlsmidm  19631  efgmf  19688  efgtf  19697  frgpuptf  19745  lmodscaf  20879  xrsds  21390  phlipf  21632  evlslem2  22057  mamucl  22366  matbas2d  22388  mamumat1cl  22404  ordtbas2  23156  iccordt  23179  txuni2  23530  xkotf  23550  txbasval  23571  tx1stc  23615  xkococn  23625  cnmpt12  23632  cnmpt21  23636  cnmpt2t  23638  cnmpt22  23639  cnmptcom  23643  cnmpt2k  23653  txswaphmeo  23770  xpstopnlem1  23774  cnmpt2plusg  24053  cnmpt2vsca  24160  prdsdsf  24332  blfvalps  24348  blfps  24371  blf  24372  stdbdmet  24481  met2ndci  24487  dscmet  24537  xrsxmet  24775  cnmpt2ds  24809  cnmpopc  24895  iimulcn  24905  ishtpy  24939  reparphti  24964  cnmpt2ip  25215  bcthlem5  25295  rrxmet  25375  dyadf  25558  itg1addlem2  25664  mbfi1fseqlem1  25682  mbfi1fseqlem3  25684  mbfi1fseqlem4  25685  mbfi1fseqlem5  25686  cxpcn3  26712  sgmf  27108  subsf  28056  midf  28844  grpodivf  30609  nvmf  30716  ipf  30784  hvsubf  31086  ofoprabco  32737  suppovss  32754  elrgspnlem2  33304  fedgmullem1  33773  fedgmullem2  33774  fedgmul  33775  sitmf  34496  cvxsconn  35425  cvmlift2lem5  35489  uncf  37920  mblfinlem1  37978  mblfinlem2  37979  sdclem1  38064  metf1o  38076  rrnval  38148  rrnmet  38150  aks6d1c3  42562  fmpocos  42675  resubf  42813  sn-subf  42861  evlselv  43020  frmx  43341  frmy  43342  ofoafg  43782  naddcnff  43790  mnringmulrcld  44655  icof  45648  fmpodg  49344  rescofuf  49568