Theorem fmpo 8022

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∀wral 3052  {csn 4582  ∪ ciun 4948   × cxp 5630  ⟶wf 6496   ∈ cmpo 7370

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 5243  ax-nul 5253  ax-pr 5379  ax-un 7690

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 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-oprab 7372  df-mpo 7373  df-1st 7943  df-2nd 7944

This theorem is referenced by:  fnmpo  8023  ovmpoelrn  8026  fmpoco  8047  eroprf  8764  omxpenlem  9018  mapxpen  9083  dffi3  9346  ixpiunwdom  9507  cantnfvalf  9586  iunfictbso  10036  axdc4lem  10377  axcclem  10379  addpqf  10867  mulpqf  10869  subf  11394  xaddf  13151  xmulf  13199  ixxf  13283  ioof  13375  fzf  13439  fzof  13584  axdc4uzlem  13918  sadcf  16392  smupf  16417  gcdf  16451  eucalgf  16522  vdwapf  16912  prdsplusg  17390  prdsmulr  17391  prdsvsca  17392  prdshom  17399  imasvscaf  17472  xpsff1o  17500  wunnat  17895  catcoppccl  18053  catcfuccl  18054  catcxpccl  18142  evlfcl  18157  hofcl  18194  mgmplusf  18587  grpsubf  18961  subgga  19241  lactghmga  19346  sylow1lem2  19540  sylow3lem1  19568  lsmssv  19584  smndlsmidm  19597  efgmf  19654  efgtf  19663  frgpuptf  19711  lmodscaf  20847  xrsds  21376  phlipf  21619  evlslem2  22046  mamucl  22357  matbas2d  22379  mamumat1cl  22395  ordtbas2  23147  iccordt  23170  txuni2  23521  xkotf  23541  txbasval  23562  tx1stc  23606  xkococn  23616  cnmpt12  23623  cnmpt21  23627  cnmpt2t  23629  cnmpt22  23630  cnmptcom  23634  cnmpt2k  23644  txswaphmeo  23761  xpstopnlem1  23765  cnmpt2plusg  24044  cnmpt2vsca  24151  prdsdsf  24323  blfvalps  24339  blfps  24362  blf  24363  stdbdmet  24472  met2ndci  24478  dscmet  24528  xrsxmet  24766  cnmpt2ds  24800  cnmpopc  24890  iimulcn  24902  iimulcnOLD  24903  ishtpy  24939  reparphti  24964  reparphtiOLD  24965  cnmpt2ip  25216  bcthlem5  25296  rrxmet  25376  dyadf  25560  itg1addlem2  25666  mbfi1fseqlem1  25684  mbfi1fseqlem3  25686  mbfi1fseqlem4  25687  mbfi1fseqlem5  25688  cxpcn3  26726  sgmf  27123  subsf  28072  midf  28860  grpodivf  30626  nvmf  30733  ipf  30801  hvsubf  31103  ofoprabco  32754  suppovss  32771  elrgspnlem2  33337  fedgmullem1  33807  fedgmullem2  33808  fedgmul  33809  sitmf  34530  cvxsconn  35459  cvmlift2lem5  35523  uncf  37850  mblfinlem1  37908  mblfinlem2  37909  sdclem1  37994  metf1o  38006  rrnval  38078  rrnmet  38080  aks6d1c3  42493  fmpocos  42606  resubf  42751  sn-subf  42799  evlselv  42945  frmx  43270  frmy  43271  ofoafg  43711  naddcnff  43719  mnringmulrcld  44584  icof  45577  fmpodg  49228  rescofuf  49452