MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fmpt2 Unicode version

Theorem fmpt2 6867
Description: Functionality, domain and range of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
Hypothesis
Ref Expression
fmpt2.1
Assertion
Ref Expression
fmpt2
Distinct variable groups:   , ,   , ,   , ,

Proof of Theorem fmpt2
StepHypRef Expression
1 fmpt2.1 . . 3
21fmpt2x 6866 . 2
3 iunxpconst 5061 . . 3
43feq2i 5729 . 2
52, 4bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  =wceq 1395  e.wcel 1818  A.wral 2807  {csn 4029  U_ciun 4330  X.cxp 5002  -->wf 5589  e.cmpt2 6298
This theorem is referenced by:  fnmpt2  6868  ovmpt2elrn  6871  fmpt2co  6883  eroprf  7428  omxpenlem  7638  mapxpen  7703  dffi3  7911  ixpiunwdom  8038  cantnfvalf  8105  iunfictbso  8516  axdc4lem  8856  axcclem  8858  addpqf  9343  mulpqf  9345  subf  9845  xaddf  11452  xmulf  11493  ixxf  11568  ioof  11651  fzf  11705  fzof  11826  axdc4uzlem  12092  sadcf  14103  smupf  14128  gcdf  14157  eucalgf  14212  vdwapf  14490  prdsval  14852  prdsplusg  14855  prdsmulr  14856  prdsvsca  14857  prdsds  14861  prdshom  14864  imasvscaf  14936  xpsff1o  14965  wunnat  15325  catcoppccl  15435  catcfuccl  15436  catcxpccl  15476  evlfcl  15491  hofcl  15528  plusffval  15877  mgmplusf  15881  grpsubf  16117  subgga  16338  lactghmga  16429  sylow1lem2  16619  sylow3lem1  16647  lsmssv  16663  lsmidm  16682  efgmf  16731  efgtf  16740  frgpuptf  16788  scaffval  17530  lmodscaf  17534  evlslem2  18180  xrsds  18461  ipffval  18683  phlipf  18687  mamucl  18903  matbas2d  18925  mamumat1cl  18941  ordtbas2  19692  iccordt  19715  txuni2  20066  xkotf  20086  txbasval  20107  tx1stc  20151  xkococn  20161  cnmpt12  20168  cnmpt21  20172  cnmpt2t  20174  cnmpt22  20175  cnmptcom  20179  cnmpt2k  20189  txswaphmeo  20306  xpstopnlem1  20310  cnmpt2plusg  20587  cnmpt2vsca  20697  prdsdsf  20870  blfvalps  20886  blfps  20909  blf  20910  stdbdmet  21019  met2ndci  21025  dscmet  21093  xrsxmet  21314  cnmpt2ds  21348  cnmpt2pc  21428  iimulcn  21438  ishtpy  21472  reparphti  21497  cnmpt2ip  21688  bcthlem5  21767  rrxmet  21835  dyadf  22000  itg1addlem2  22104  mbfi1fseqlem1  22122  mbfi1fseqlem3  22124  mbfi1fseqlem4  22125  mbfi1fseqlem5  22126  cxpcn3  23122  sgmf  23419  midf  24142  grpodivf  25248  nvmf  25541  ipf  25626  hvsubf  25932  ofoprabco  27505  sseqfv2  28333  cvxscon  28688  cvmlift2lem5  28752  mblfinlem1  30051  mblfinlem2  30052  sdclem1  30236  metf1o  30248  rrnval  30323  rrnmet  30325  frmx  30849  frmy  30850
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-fv 5601  df-oprab 6300  df-mpt2 6301  df-1st 6800  df-2nd 6801
  Copyright terms: Public domain W3C validator