Theorem fmpo 7955

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

Syntax hints:   ↔ wb 205   = wceq 1540   ∈ wcel 2105  ∀wral 3062  {csn 4571  ∪ ciun 4937   × cxp 5606  ⟶wf 6462   ∈ cmpo 7319

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pr 5367  ax-un 7630

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-iun 4939  df-br 5088  df-opab 5150  df-mpt 5171  df-id 5507  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621  df-iota 6418  df-fun 6468  df-fn 6469  df-f 6470  df-fv 6474  df-oprab 7321  df-mpo 7322  df-1st 7878  df-2nd 7879

This theorem is referenced by:  fnmpo  7956  ovmpoelrn  7959  fmpoco  7982  eroprf  8654  omxpenlem  8917  mapxpen  8987  dffi3  9267  ixpiunwdom  9426  cantnfvalf  9501  iunfictbso  9950  axdc4lem  10291  axcclem  10293  addpqf  10780  mulpqf  10782  subf  11303  xaddf  13038  xmulf  13086  ixxf  13169  ioof  13259  fzf  13323  fzof  13464  axdc4uzlem  13783  sadcf  16239  smupf  16264  gcdf  16298  eucalgf  16365  vdwapf  16750  prdsplusg  17246  prdsmulr  17247  prdsvsca  17248  prdshom  17255  imasvscaf  17327  xpsff1o  17355  wunnat  17749  wunnatOLD  17750  catcoppccl  17909  catcoppcclOLD  17910  catcfuccl  17911  catcfucclOLD  17912  catcxpccl  18001  catcxpcclOLD  18002  evlfcl  18017  hofcl  18054  mgmplusf  18413  grpsubf  18730  subgga  18982  lactghmga  19089  sylow1lem2  19280  sylow3lem1  19308  lsmssv  19324  smndlsmidm  19337  efgmf  19394  efgtf  19403  frgpuptf  19451  lmodscaf  20228  xrsds  20724  phlipf  20940  evlslem2  21372  mamucl  21631  matbas2d  21655  mamumat1cl  21671  ordtbas2  22425  iccordt  22448  txuni2  22799  xkotf  22819  txbasval  22840  tx1stc  22884  xkococn  22894  cnmpt12  22901  cnmpt21  22905  cnmpt2t  22907  cnmpt22  22908  cnmptcom  22912  cnmpt2k  22922  txswaphmeo  23039  xpstopnlem1  23043  cnmpt2plusg  23322  cnmpt2vsca  23429  prdsdsf  23603  blfvalps  23619  blfps  23642  blf  23643  stdbdmet  23755  met2ndci  23761  dscmet  23811  xrsxmet  24055  cnmpt2ds  24089  cnmpopc  24174  iimulcn  24184  ishtpy  24218  reparphti  24243  cnmpt2ip  24495  bcthlem5  24575  rrxmet  24655  dyadf  24838  itg1addlem2  24944  mbfi1fseqlem1  24963  mbfi1fseqlem3  24965  mbfi1fseqlem4  24966  mbfi1fseqlem5  24967  cxpcn3  25984  sgmf  26377  midf  27273  grpodivf  29036  nvmf  29143  ipf  29211  hvsubf  29513  ofoprabco  31136  suppovss  31152  fedgmullem1  31850  fedgmullem2  31851  fedgmul  31852  sitmf  32459  cvxsconn  33344  cvmlift2lem5  33408  uncf  35828  mblfinlem1  35886  mblfinlem2  35887  sdclem1  35973  metf1o  35985  rrnval  36057  rrnmet  36059  resubf  40580  sn-subf  40626  frmx  40952  frmy  40953  ofoafg  41266  naddcnff  41274  mnringmulrcld  42080  icof  43000