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

Theorem mpt20 6429
 Description: A mapping operation with empty domain. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Revised by Mario Carneiro, 15-May-2015.)
Assertion
Ref Expression
mpt20

Proof of Theorem mpt20
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-mpt2 6088 . 2
2 df-oprab 6087 . 2
3 noel 3634 . . . . . . 7
4 simprll 740 . . . . . . 7
53, 4mto 170 . . . . . 6
65nex 1565 . . . . 5
76nex 1565 . . . 4
87nex 1565 . . 3
98abf 3663 . 2
101, 2, 93eqtri 2462 1
 Colors of variables: wff set class Syntax hints:   wa 360  wex 1551   wceq 1653   wcel 1726  cab 2424  c0 3630  cop 3819  coprab 6084   cmpt2 6085 This theorem is referenced by:  homffval  13919  comfffval  13926  natfval  14145  coafval  14221  xpchomfval  14278  xpccofval  14281  meet0  14566  join0  14567  plusffval  14704  grpsubfval  14849  oppglsm  15278  dvrfval  15791  scaffval  15970  psrmulr  16450  ipffval  16881  pcofval  19037  mendplusgfval  27472  mendmulrfval  27474  mendvscafval  27477 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-dif 3325  df-in 3329  df-ss 3336  df-nul 3631  df-oprab 6087  df-mpt2 6088
 Copyright terms: Public domain W3C validator