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

Theorem fmpt2 7438
 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:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝐷,𝑦
Allowed substitution hints:   𝐶(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem fmpt2
StepHypRef Expression
1 fmpt2.1 . . 3 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
21fmpt2x 7437 . 2 (∀𝑥𝐴𝑦𝐵 𝐶𝐷𝐹: 𝑥𝐴 ({𝑥} × 𝐵)⟶𝐷)
3 iunxpconst 5343 . . 3 𝑥𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵)
43feq2i 6215 . 2 (𝐹: 𝑥𝐴 ({𝑥} × 𝐵)⟶𝐷𝐹:(𝐴 × 𝐵)⟶𝐷)
52, 4bitri 266 1 (∀𝑥𝐴𝑦𝐵 𝐶𝐷𝐹:(𝐴 × 𝐵)⟶𝐷)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 197   = wceq 1652   ∈ wcel 2155  ∀wral 3055  {csn 4334  ∪ ciun 4676   × cxp 5275  ⟶wf 6064   ↦ cmpt2 6844 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147 This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-fv 6076  df-oprab 6846  df-mpt2 6847  df-1st 7366  df-2nd 7367 This theorem is referenced by:  fnmpt2  7439  ovmpt2elrn  7442  fmpt2co  7462  eroprf  8049  omxpenlem  8268  mapxpen  8333  dffi3  8544  ixpiunwdom  8703  cantnfvalf  8777  iunfictbso  9188  axdc4lem  9530  axcclem  9532  addpqf  10019  mulpqf  10021  subf  10537  xaddf  12257  xmulf  12304  ixxf  12387  ioof  12474  fzf  12537  fzof  12675  axdc4uzlem  12990  sadcf  15456  smupf  15481  gcdf  15515  eucalgf  15577  vdwapf  15955  prdsval  16381  prdsplusg  16384  prdsmulr  16385  prdsvsca  16386  prdsds  16390  prdshom  16393  imasvscaf  16465  xpsff1o  16494  wunnat  16881  catcoppccl  17023  catcfuccl  17024  catcxpccl  17113  evlfcl  17128  hofcl  17165  plusffval  17513  mgmplusf  17517  grpsubf  17761  subgga  17996  lactghmga  18087  sylow1lem2  18278  sylow3lem1  18306  lsmssv  18322  lsmidm  18341  efgmf  18390  efgtf  18399  frgpuptf  18449  scaffval  19150  lmodscaf  19154  evlslem2  19785  xrsds  20062  ipffval  20268  phlipf  20272  mamucl  20483  matbas2d  20505  mamumat1cl  20521  ordtbas2  21275  iccordt  21298  txuni2  21648  xkotf  21668  txbasval  21689  tx1stc  21733  xkococn  21743  cnmpt12  21750  cnmpt21  21754  cnmpt2t  21756  cnmpt22  21757  cnmptcom  21761  cnmpt2k  21771  txswaphmeo  21888  xpstopnlem1  21892  cnmpt2plusg  22171  cnmpt2vsca  22277  prdsdsf  22451  blfvalps  22467  blfps  22490  blf  22491  stdbdmet  22600  met2ndci  22606  dscmet  22656  xrsxmet  22891  cnmpt2ds  22925  cnmpt2pc  23006  iimulcn  23016  ishtpy  23050  reparphti  23075  cnmpt2ip  23325  bcthlem5  23405  rrxmet  23480  dyadf  23649  itg1addlem2  23755  mbfi1fseqlem1  23773  mbfi1fseqlem3  23775  mbfi1fseqlem4  23776  mbfi1fseqlem5  23777  cxpcn3  24780  sgmf  25162  midf  25959  grpodivf  27849  nvmf  27956  ipf  28024  hvsubf  28328  ofoprabco  29914  sitmf  30861  cvxsconn  31673  cvmlift2lem5  31737  uncf  33812  mblfinlem1  33870  mblfinlem2  33871  sdclem1  33961  metf1o  33973  rrnval  34048  rrnmet  34050  frmx  38155  frmy  38156  icof  40056
 Copyright terms: Public domain W3C validator