Theorem fmpo 8094

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

Syntax hints:   ↔ wb 206   = wceq 1539   ∈ wcel 2107  ∀wral 3060  {csn 4625  ∪ ciun 4990   × cxp 5682  ⟶wf 6556   ∈ cmpo 7434

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431  ax-un 7756

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-fv 6568  df-oprab 7436  df-mpo 7437  df-1st 8015  df-2nd 8016

This theorem is referenced by:  fnmpo  8095  ovmpoelrn  8098  fmpoco  8121  eroprf  8856  omxpenlem  9114  mapxpen  9184  dffi3  9472  ixpiunwdom  9631  cantnfvalf  9706  iunfictbso  10155  axdc4lem  10496  axcclem  10498  addpqf  10985  mulpqf  10987  subf  11511  xaddf  13267  xmulf  13315  ixxf  13398  ioof  13488  fzf  13552  fzof  13697  axdc4uzlem  14025  sadcf  16491  smupf  16516  gcdf  16550  eucalgf  16621  vdwapf  17011  prdsplusg  17504  prdsmulr  17505  prdsvsca  17506  prdshom  17513  imasvscaf  17585  xpsff1o  17613  wunnat  18005  catcoppccl  18163  catcfuccl  18164  catcxpccl  18253  evlfcl  18268  hofcl  18305  mgmplusf  18664  grpsubf  19038  subgga  19319  lactghmga  19424  sylow1lem2  19618  sylow3lem1  19646  lsmssv  19662  smndlsmidm  19675  efgmf  19732  efgtf  19741  frgpuptf  19789  lmodscaf  20883  xrsds  21428  phlipf  21671  evlslem2  22104  mamucl  22406  matbas2d  22430  mamumat1cl  22446  ordtbas2  23200  iccordt  23223  txuni2  23574  xkotf  23594  txbasval  23615  tx1stc  23659  xkococn  23669  cnmpt12  23676  cnmpt21  23680  cnmpt2t  23682  cnmpt22  23683  cnmptcom  23687  cnmpt2k  23697  txswaphmeo  23814  xpstopnlem1  23818  cnmpt2plusg  24097  cnmpt2vsca  24204  prdsdsf  24378  blfvalps  24394  blfps  24417  blf  24418  stdbdmet  24530  met2ndci  24536  dscmet  24586  xrsxmet  24832  cnmpt2ds  24866  cnmpopc  24956  iimulcn  24968  iimulcnOLD  24969  ishtpy  25005  reparphti  25030  reparphtiOLD  25031  cnmpt2ip  25283  bcthlem5  25363  rrxmet  25443  dyadf  25627  itg1addlem2  25733  mbfi1fseqlem1  25751  mbfi1fseqlem3  25753  mbfi1fseqlem4  25754  mbfi1fseqlem5  25755  cxpcn3  26792  sgmf  27189  subsf  28095  midf  28785  grpodivf  30558  nvmf  30665  ipf  30733  hvsubf  31035  ofoprabco  32675  suppovss  32691  elrgspnlem2  33248  fedgmullem1  33681  fedgmullem2  33682  fedgmul  33683  sitmf  34355  cvxsconn  35249  cvmlift2lem5  35313  uncf  37607  mblfinlem1  37665  mblfinlem2  37666  sdclem1  37751  metf1o  37763  rrnval  37835  rrnmet  37837  aks6d1c3  42125  fmpocos  42275  resubf  42416  sn-subf  42463  evlselv  42602  frmx  42930  frmy  42931  ofoafg  43372  naddcnff  43380  mnringmulrcld  44252  icof  45229  fmpodg  48775  rescofuf  48940