Theorem fmpo 8061

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

Syntax hints:   ↔ wb 209   = wceq 1570   ∈ wcel 2143  ∀wral 3079  {csn 4589  ∪ ciun 4956   × cxp 5659  ⟶wf 6532   ∈ cmpo 7412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-oprab 7414  df-mpo 7415  df-1st 7982  df-2nd 7983

This theorem is referenced by:  fnmpo  8062  ovmpoelrn  8065  fmpoco  8086  eroprf  8809  omxpenlem  9062  mapxpen  9127  dffi3  9387  ixpiunwdom  9548  cantnfvalf  9630  iunfictbso  10094  axdc4lem  10434  axcclem  10436  addpqf  10924  mulpqf  10926  subf  11454  xaddf  13245  xmulf  13293  ixxf  13377  ioof  13469  fzf  13534  fzof  13680  axdc4uzlem  14015  sadcf  16506  smupf  16531  gcdf  16565  eucalgf  16636  vdwapf  17027  prdsplusg  17506  prdsmulr  17507  prdsvsca  17508  prdshom  17515  imasvscaf  17588  xpsff1o  17616  wunnat  18011  catcoppccl  18169  catcfuccl  18170  catcxpccl  18258  evlfcl  18273  hofcl  18310  mgmplusf  18703  grpsubf  19080  subgga  19365  lactghmga  19470  sylow1lem2  19664  sylow3lem1  19692  lsmssv  19708  smndlsmidm  19721  efgmf  19778  efgtf  19787  frgpuptf  19835  lmodscaf  21005  xrsds  21560  phlipf  21802  evlslem2  22230  mamucl  22558  matbas2d  22580  mamumat1cl  22596  ordtbas2  23348  iccordt  23371  txuni2  23722  xkotf  23742  txbasval  23763  tx1stc  23807  xkococn  23817  cnmpt12  23824  cnmpt21  23828  cnmpt2t  23830  cnmpt22  23831  cnmptcom  23835  cnmpt2k  23845  txswaphmeo  23962  xpstopnlem1  23966  cnmpt2plusg  24245  cnmpt2vsca  24352  prdsdsf  24524  blfvalps  24540  blfps  24563  blf  24564  stdbdmet  24673  met2ndci  24679  dscmet  24729  xrsxmet  24967  cnmpt2ds  25001  cnmpopc  25087  iimulcn  25097  ishtpy  25131  reparphti  25156  cnmpt2ip  25407  bcthlem5  25487  rrxmet  25567  dyadf  25750  itg1addlem2  25856  mbfi1fseqlem1  25874  mbfi1fseqlem3  25876  mbfi1fseqlem4  25877  mbfi1fseqlem5  25878  cxpcn3  26913  sgmf  27309  subsf  28257  midf  29085  grpodivf  30890  nvmf  30997  ipf  31065  hvsubf  31367  ofoprabco  33009  suppovss  33026  elrgspnlem2  33563  fedgmullem1  34019  fedgmullem2  34020  fedgmul  34021  sitmf  34742  cvxsconn  35735  cvmlift2lem5  35799  uncf  38250  mblfinlem1  38308  mblfinlem2  38309  sdclem1  38394  metf1o  38406  rrnval  38478  rrnmet  38480  aks6d1c3  42890  fmpocos  43004  resubf  43142  sn-subf  43190  evlselv  43321  frmx  43640  frmy  43641  ofoafg  44081  naddcnff  44089  mnringmulrcld  44952  icof  45935  fmpodg  49647  rescofuf  49871