Theorem fmpo 8056

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

Syntax hints:   ↔ wb 205   = wceq 1541   ∈ wcel 2106  ∀wral 3061  {csn 4628  ∪ ciun 4997   × cxp 5674  ⟶wf 6539   ∈ cmpo 7413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-oprab 7415  df-mpo 7416  df-1st 7977  df-2nd 7978

This theorem is referenced by:  fnmpo  8057  ovmpoelrn  8060  fmpoco  8083  eroprf  8811  omxpenlem  9075  mapxpen  9145  dffi3  9428  ixpiunwdom  9587  cantnfvalf  9662  iunfictbso  10111  axdc4lem  10452  axcclem  10454  addpqf  10941  mulpqf  10943  subf  11464  xaddf  13205  xmulf  13253  ixxf  13336  ioof  13426  fzf  13490  fzof  13631  axdc4uzlem  13950  sadcf  16396  smupf  16421  gcdf  16455  eucalgf  16522  vdwapf  16907  prdsplusg  17406  prdsmulr  17407  prdsvsca  17408  prdshom  17415  imasvscaf  17487  xpsff1o  17515  wunnat  17909  wunnatOLD  17910  catcoppccl  18069  catcoppcclOLD  18070  catcfuccl  18071  catcfucclOLD  18072  catcxpccl  18161  catcxpcclOLD  18162  evlfcl  18177  hofcl  18214  mgmplusf  18573  grpsubf  18904  subgga  19166  lactghmga  19275  sylow1lem2  19469  sylow3lem1  19497  lsmssv  19513  smndlsmidm  19526  efgmf  19583  efgtf  19592  frgpuptf  19640  lmodscaf  20499  xrsds  20994  phlipf  21211  evlslem2  21648  mamucl  21908  matbas2d  21932  mamumat1cl  21948  ordtbas2  22702  iccordt  22725  txuni2  23076  xkotf  23096  txbasval  23117  tx1stc  23161  xkococn  23171  cnmpt12  23178  cnmpt21  23182  cnmpt2t  23184  cnmpt22  23185  cnmptcom  23189  cnmpt2k  23199  txswaphmeo  23316  xpstopnlem1  23320  cnmpt2plusg  23599  cnmpt2vsca  23706  prdsdsf  23880  blfvalps  23896  blfps  23919  blf  23920  stdbdmet  24032  met2ndci  24038  dscmet  24088  xrsxmet  24332  cnmpt2ds  24366  cnmpopc  24451  iimulcn  24461  ishtpy  24495  reparphti  24520  cnmpt2ip  24772  bcthlem5  24852  rrxmet  24932  dyadf  25115  itg1addlem2  25221  mbfi1fseqlem1  25240  mbfi1fseqlem3  25242  mbfi1fseqlem4  25243  mbfi1fseqlem5  25244  cxpcn3  26263  sgmf  26656  midf  28065  grpodivf  29829  nvmf  29936  ipf  30004  hvsubf  30306  ofoprabco  31927  suppovss  31944  fedgmullem1  32773  fedgmullem2  32774  fedgmul  32775  sitmf  33420  cvxsconn  34303  cvmlift2lem5  34367  gg-iimulcn  35244  gg-reparphti  35247  uncf  36559  mblfinlem1  36617  mblfinlem2  36618  sdclem1  36703  metf1o  36715  rrnval  36787  rrnmet  36789  fmpocos  41148  evlselv  41247  resubf  41342  sn-subf  41389  frmx  41740  frmy  41741  ofoafg  42192  naddcnff  42200  mnringmulrcld  43075  icof  44003