Theorem fmpo 7766

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

Syntax hints:   ↔ wb 208   = wceq 1537   ∈ wcel 2114  ∀wral 3138  {csn 4567  ∪ ciun 4919   × cxp 5553  ⟶wf 6351   ∈ cmpo 7158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-fv 6363  df-oprab 7160  df-mpo 7161  df-1st 7689  df-2nd 7690

This theorem is referenced by:  fnmpo  7767  ovmpoelrn  7770  fmpoco  7790  eroprf  8395  omxpenlem  8618  mapxpen  8683  dffi3  8895  ixpiunwdom  9055  cantnfvalf  9128  iunfictbso  9540  axdc4lem  9877  axcclem  9879  addpqf  10366  mulpqf  10368  subf  10888  xaddf  12618  xmulf  12666  ixxf  12749  ioof  12836  fzf  12897  fzof  13036  axdc4uzlem  13352  sadcf  15802  smupf  15827  gcdf  15861  eucalgf  15927  vdwapf  16308  prdsval  16728  prdsplusg  16731  prdsmulr  16732  prdsvsca  16733  prdsds  16737  prdshom  16740  imasvscaf  16812  xpsff1o  16840  wunnat  17226  catcoppccl  17368  catcfuccl  17369  catcxpccl  17457  evlfcl  17472  hofcl  17509  mgmplusf  17862  grpsubf  18178  subgga  18430  lactghmga  18533  sylow1lem2  18724  sylow3lem1  18752  lsmssv  18768  smndlsmidm  18781  lsmidmOLD  18789  efgmf  18839  efgtf  18848  frgpuptf  18896  lmodscaf  19656  evlslem2  20292  xrsds  20588  phlipf  20796  mamucl  21010  matbas2d  21032  mamumat1cl  21048  ordtbas2  21799  iccordt  21822  txuni2  22173  xkotf  22193  txbasval  22214  tx1stc  22258  xkococn  22268  cnmpt12  22275  cnmpt21  22279  cnmpt2t  22281  cnmpt22  22282  cnmptcom  22286  cnmpt2k  22296  txswaphmeo  22413  xpstopnlem1  22417  cnmpt2plusg  22696  cnmpt2vsca  22803  prdsdsf  22977  blfvalps  22993  blfps  23016  blf  23017  stdbdmet  23126  met2ndci  23132  dscmet  23182  xrsxmet  23417  cnmpt2ds  23451  cnmpopc  23532  iimulcn  23542  ishtpy  23576  reparphti  23601  cnmpt2ip  23851  bcthlem5  23931  rrxmet  24011  dyadf  24192  itg1addlem2  24298  mbfi1fseqlem1  24316  mbfi1fseqlem3  24318  mbfi1fseqlem4  24319  mbfi1fseqlem5  24320  cxpcn3  25329  sgmf  25722  midf  26562  grpodivf  28315  nvmf  28422  ipf  28490  hvsubf  28792  ofoprabco  30409  suppovss  30426  fedgmullem1  31025  fedgmullem2  31026  fedgmul  31027  sitmf  31610  cvxsconn  32490  cvmlift2lem5  32554  uncf  34886  mblfinlem1  34944  mblfinlem2  34945  sdclem1  35033  metf1o  35045  rrnval  35120  rrnmet  35122  resubf  39260  frmx  39559  frmy  39560  icof  41531