Theorem fmpo 8026

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∀wral 3044  {csn 4585  ∪ ciun 4951   × cxp 5629  ⟶wf 6495   ∈ cmpo 7371

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 5246  ax-nul 5256  ax-pr 5382  ax-un 7691

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 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-fv 6507  df-oprab 7373  df-mpo 7374  df-1st 7947  df-2nd 7948

This theorem is referenced by:  fnmpo  8027  ovmpoelrn  8030  fmpoco  8051  eroprf  8765  omxpenlem  9019  mapxpen  9084  dffi3  9358  ixpiunwdom  9519  cantnfvalf  9594  iunfictbso  10043  axdc4lem  10384  axcclem  10386  addpqf  10873  mulpqf  10875  subf  11399  xaddf  13160  xmulf  13208  ixxf  13292  ioof  13384  fzf  13448  fzof  13593  axdc4uzlem  13924  sadcf  16399  smupf  16424  gcdf  16458  eucalgf  16529  vdwapf  16919  prdsplusg  17397  prdsmulr  17398  prdsvsca  17399  prdshom  17406  imasvscaf  17478  xpsff1o  17506  wunnat  17897  catcoppccl  18055  catcfuccl  18056  catcxpccl  18144  evlfcl  18159  hofcl  18196  mgmplusf  18553  grpsubf  18927  subgga  19208  lactghmga  19311  sylow1lem2  19505  sylow3lem1  19533  lsmssv  19549  smndlsmidm  19562  efgmf  19619  efgtf  19628  frgpuptf  19676  lmodscaf  20766  xrsds  21302  phlipf  21537  evlslem2  21962  mamucl  22264  matbas2d  22286  mamumat1cl  22302  ordtbas2  23054  iccordt  23077  txuni2  23428  xkotf  23448  txbasval  23469  tx1stc  23513  xkococn  23523  cnmpt12  23530  cnmpt21  23534  cnmpt2t  23536  cnmpt22  23537  cnmptcom  23541  cnmpt2k  23551  txswaphmeo  23668  xpstopnlem1  23672  cnmpt2plusg  23951  cnmpt2vsca  24058  prdsdsf  24231  blfvalps  24247  blfps  24270  blf  24271  stdbdmet  24380  met2ndci  24386  dscmet  24436  xrsxmet  24674  cnmpt2ds  24708  cnmpopc  24798  iimulcn  24810  iimulcnOLD  24811  ishtpy  24847  reparphti  24872  reparphtiOLD  24873  cnmpt2ip  25124  bcthlem5  25204  rrxmet  25284  dyadf  25468  itg1addlem2  25574  mbfi1fseqlem1  25592  mbfi1fseqlem3  25594  mbfi1fseqlem4  25595  mbfi1fseqlem5  25596  cxpcn3  26634  sgmf  27031  subsf  27944  midf  28679  grpodivf  30440  nvmf  30547  ipf  30615  hvsubf  30917  ofoprabco  32561  suppovss  32577  elrgspnlem2  33167  fedgmullem1  33598  fedgmullem2  33599  fedgmul  33600  sitmf  34316  cvxsconn  35203  cvmlift2lem5  35267  uncf  37566  mblfinlem1  37624  mblfinlem2  37625  sdclem1  37710  metf1o  37722  rrnval  37794  rrnmet  37796  aks6d1c3  42084  fmpocos  42195  resubf  42342  sn-subf  42390  evlselv  42548  frmx  42875  frmy  42876  ofoafg  43316  naddcnff  43324  mnringmulrcld  44190  icof  45186  fmpodg  48830  rescofuf  49055