Theorem fmpo 8047

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∀wral 3044  {csn 4589  ∪ ciun 4955   × cxp 5636  ⟶wf 6507   ∈ cmpo 7389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-oprab 7391  df-mpo 7392  df-1st 7968  df-2nd 7969

This theorem is referenced by:  fnmpo  8048  ovmpoelrn  8051  fmpoco  8074  eroprf  8788  omxpenlem  9042  mapxpen  9107  dffi3  9382  ixpiunwdom  9543  cantnfvalf  9618  iunfictbso  10067  axdc4lem  10408  axcclem  10410  addpqf  10897  mulpqf  10899  subf  11423  xaddf  13184  xmulf  13232  ixxf  13316  ioof  13408  fzf  13472  fzof  13617  axdc4uzlem  13948  sadcf  16423  smupf  16448  gcdf  16482  eucalgf  16553  vdwapf  16943  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  prdshom  17430  imasvscaf  17502  xpsff1o  17530  wunnat  17921  catcoppccl  18079  catcfuccl  18080  catcxpccl  18168  evlfcl  18183  hofcl  18220  mgmplusf  18577  grpsubf  18951  subgga  19232  lactghmga  19335  sylow1lem2  19529  sylow3lem1  19557  lsmssv  19573  smndlsmidm  19586  efgmf  19643  efgtf  19652  frgpuptf  19700  lmodscaf  20790  xrsds  21326  phlipf  21561  evlslem2  21986  mamucl  22288  matbas2d  22310  mamumat1cl  22326  ordtbas2  23078  iccordt  23101  txuni2  23452  xkotf  23472  txbasval  23493  tx1stc  23537  xkococn  23547  cnmpt12  23554  cnmpt21  23558  cnmpt2t  23560  cnmpt22  23561  cnmptcom  23565  cnmpt2k  23575  txswaphmeo  23692  xpstopnlem1  23696  cnmpt2plusg  23975  cnmpt2vsca  24082  prdsdsf  24255  blfvalps  24271  blfps  24294  blf  24295  stdbdmet  24404  met2ndci  24410  dscmet  24460  xrsxmet  24698  cnmpt2ds  24732  cnmpopc  24822  iimulcn  24834  iimulcnOLD  24835  ishtpy  24871  reparphti  24896  reparphtiOLD  24897  cnmpt2ip  25148  bcthlem5  25228  rrxmet  25308  dyadf  25492  itg1addlem2  25598  mbfi1fseqlem1  25616  mbfi1fseqlem3  25618  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  cxpcn3  26658  sgmf  27055  subsf  27968  midf  28703  grpodivf  30467  nvmf  30574  ipf  30642  hvsubf  30944  ofoprabco  32588  suppovss  32604  elrgspnlem2  33194  fedgmullem1  33625  fedgmullem2  33626  fedgmul  33627  sitmf  34343  cvxsconn  35230  cvmlift2lem5  35294  uncf  37593  mblfinlem1  37651  mblfinlem2  37652  sdclem1  37737  metf1o  37749  rrnval  37821  rrnmet  37823  aks6d1c3  42111  fmpocos  42222  resubf  42369  sn-subf  42417  evlselv  42575  frmx  42902  frmy  42903  ofoafg  43343  naddcnff  43351  mnringmulrcld  44217  icof  45213  fmpodg  48854  rescofuf  49079