Theorem fmpo 8071

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2146  ∀wral 3081  {csn 4591  ∪ ciun 4958   × cxp 5661  ⟶wf 6536   ∈ cmpo 7421

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 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7742

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-oprab 7423  df-mpo 7424  df-1st 7992  df-2nd 7993

This theorem is used by:  fnmpo  8072  ovmpoelrn  8075  fmpoco  8096  eroprf  8819  omxpenlem  9073  mapxpen  9138  dffi3  9398  ixpiunwdom  9559  cantnfvalf  9641  iunfictbso  10114  axdc4lem  10454  axcclem  10456  addpqf  10944  mulpqf  10946  subf  11474  xaddf  13266  xmulf  13314  ixxf  13398  ioof  13490  fzf  13555  fzof  13701  axdc4uzlem  14037  sadcf  16533  smupf  16558  gcdf  16592  eucalgf  16663  vdwapf  17054  prdsplusg  17533  prdsmulr  17534  prdsvsca  17535  prdshom  17542  imasvscaf  17615  xpsff1o  17643  wunnat  18038  catcoppccl  18196  catcfuccl  18197  catcxpccl  18285  evlfcl  18300  hofcl  18337  mgmplusf  18730  grpsubf  19129  subgga  19414  lactghmga  19519  sylow1lem2  19713  sylow3lem1  19741  lsmssv  19757  smndlsmidm  19770  efgmf  19827  efgtf  19836  frgpuptf  19884  lmodscaf  21055  xrsds  21610  phlipf  21852  evlslem2  22280  mamucl  22608  matbas2d  22630  mamumat1cl  22646  ordtbas2  23398  iccordt  23421  txuni2  23773  xkotf  23793  txbasval  23814  tx1stc  23858  xkococn  23868  cnmpt12  23875  cnmpt21  23879  cnmpt2t  23881  cnmpt22  23882  cnmptcom  23886  cnmpt2k  23896  txswaphmeo  24013  xpstopnlem1  24017  cnmpt2plusg  24296  cnmpt2vsca  24403  prdsdsf  24575  blfvalps  24591  blfps  24614  blf  24615  stdbdmet  24724  met2ndci  24730  dscmet  24780  xrsxmet  25018  cnmpt2ds  25052  cnmpopc  25138  iimulcn  25148  ishtpy  25182  reparphti  25207  cnmpt2ip  25458  bcthlem5  25538  rrxmet  25618  dyadf  25801  itg1addlem2  25907  mbfi1fseqlem1  25925  mbfi1fseqlem3  25927  mbfi1fseqlem4  25928  mbfi1fseqlem5  25929  cxpcn3  26964  sgmf  27360  subsf  28308  midf  29136  grpodivf  30961  nvmf  31068  ipf  31136  hvsubf  31438  ofoprabco  33080  suppovss  33097  elrgspnlem2  33627  fedgmullem1  34083  fedgmullem2  34084  fedgmul  34085  sitmf  34807  cvxsconn  35772  cvmlift2lem5  35836  uncf  38307  mblfinlem1  38365  mblfinlem2  38366  sdclem1  38452  metf1o  38464  rrnval  38536  rrnmet  38538  aks6d1c3  42948  fmpocos  43062  resubf  43200  sn-subf  43248  evlselv  43379  frmx  43698  frmy  43699  ofoafg  44139  naddcnff  44147  mnringmulrcld  45010  icof  45993  fmpodg  49704  rescofuf  49928