Theorem fmpo 8074

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2146  ∀wral 3082  {csn 4594  ∪ ciun 4961   × cxp 5664  ⟶wf 6539   ∈ cmpo 7425

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409  ax-un 7745

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-oprab 7427  df-mpo 7428  df-1st 7995  df-2nd 7996

This theorem is used by:  fnmpo  8075  ovmpoelrn  8078  fmpoco  8099  eroprf  8822  omxpenlem  9076  mapxpen  9141  dffi3  9401  ixpiunwdom  9562  cantnfvalf  9644  iunfictbso  10117  axdc4lem  10457  axcclem  10459  addpqf  10947  mulpqf  10949  subf  11477  xaddf  13268  xmulf  13316  ixxf  13400  ioof  13492  fzf  13557  fzof  13703  axdc4uzlem  14039  sadcf  16536  smupf  16561  gcdf  16595  eucalgf  16666  vdwapf  17057  prdsplusg  17536  prdsmulr  17537  prdsvsca  17538  prdshom  17545  imasvscaf  17618  xpsff1o  17646  wunnat  18041  catcoppccl  18199  catcfuccl  18200  catcxpccl  18288  evlfcl  18303  hofcl  18340  mgmplusf  18733  grpsubf  19110  subgga  19395  lactghmga  19500  sylow1lem2  19694  sylow3lem1  19722  lsmssv  19738  smndlsmidm  19751  efgmf  19808  efgtf  19817  frgpuptf  19865  lmodscaf  21035  xrsds  21590  phlipf  21832  evlslem2  22260  mamucl  22588  matbas2d  22610  mamumat1cl  22626  ordtbas2  23378  iccordt  23401  txuni2  23752  xkotf  23772  txbasval  23793  tx1stc  23837  xkococn  23847  cnmpt12  23854  cnmpt21  23858  cnmpt2t  23860  cnmpt22  23861  cnmptcom  23865  cnmpt2k  23875  txswaphmeo  23992  xpstopnlem1  23996  cnmpt2plusg  24275  cnmpt2vsca  24382  prdsdsf  24554  blfvalps  24570  blfps  24593  blf  24594  stdbdmet  24703  met2ndci  24709  dscmet  24759  xrsxmet  24997  cnmpt2ds  25031  cnmpopc  25117  iimulcn  25127  ishtpy  25161  reparphti  25186  cnmpt2ip  25437  bcthlem5  25517  rrxmet  25597  dyadf  25780  itg1addlem2  25886  mbfi1fseqlem1  25904  mbfi1fseqlem3  25906  mbfi1fseqlem4  25907  mbfi1fseqlem5  25908  cxpcn3  26943  sgmf  27339  subsf  28287  midf  29115  grpodivf  30920  nvmf  31027  ipf  31095  hvsubf  31397  ofoprabco  33039  suppovss  33056  elrgspnlem2  33587  fedgmullem1  34043  fedgmullem2  34044  fedgmul  34045  sitmf  34766  cvxsconn  35748  cvmlift2lem5  35812  uncf  38283  mblfinlem1  38341  mblfinlem2  38342  sdclem1  38427  metf1o  38439  rrnval  38511  rrnmet  38513  aks6d1c3  42923  fmpocos  43037  resubf  43175  sn-subf  43223  evlselv  43354  frmx  43673  frmy  43674  ofoafg  44114  naddcnff  44122  mnringmulrcld  44985  icof  45968  fmpodg  49680  rescofuf  49904