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

Theorem 19.21v 1729
Description: Version of 19.21 1905 with a dv condition.

Notational convention: We sometimes suffix with "v" the label of a theorem using a distinct variable ("dv") condition instead of a non-freeness hypothesis such as . Conversely, we sometimes suffix with "f" the label of a theorem introducing such a non-freeness hypothesis ("f" stands for "not free in", see df-nf 1617) instead of a dv condition. For instance, 19.21v 1729 versus 19.21 1905 and vtoclf 3160 versus vtocl 3161. Note that "not free in" is less restrictive than "does not occur in." Note that the version with a dv condition is easily proved from the version with the corresponding non-freeness hypothesis, by using nfv 1707. However, the dv version can often be proved from fewer axioms. (Contributed by NM, 21-Jun-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-2020.)

Assertion
Ref Expression
19.21v
Distinct variable group:   ,

Proof of Theorem 19.21v
StepHypRef Expression
1 ax-5 1704 . . 3
2 alim 1632 . . 3
31, 2syl5 32 . 2
4 ax5e 1706 . . . 4
54imim1i 58 . . 3
6 19.38 1662 . . 3
75, 6syl 16 . 2
83, 7impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  E.wex 1612
This theorem is referenced by:  19.32v  1730  stdpc5v  1732  pm11.53v  1764  19.12vvv  1765  pm11.53  1983  19.12vv  1986  cbval2  2027  sbhb  2182  2sb6  2188  r2al  2835  r3al  2837  r19.21v  2862  r3alOLD  2895  ceqsralt  3133  euind  3286  reu2  3287  reuind  3303  unissb  4281  dfiin2g  4363  axrep5  4568  asymref  5388  fvn0ssdmfun  6022  dff13  6166  mpt22eqb  6411  findcard3  7783  marypha1lem  7913  marypha2lem3  7917  aceq1  8519  kmlem15  8565  dfon2lem8  29222  dffun10  29564  mpt2bi123f  30571  mptbi12f  30575  pm10.541  31272  pm10.542  31273  19.21vv  31281  pm11.62  31300  2sbc6g  31322  2rexsb  32175  bnj864  33980  bnj865  33981  bnj978  34007  bnj1176  34061  bnj1186  34063  bj-cbval2v  34302  bj-axrep5  34378  bj-ralcom4  34444  cotr2g  37786  dfhe3  37799
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
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator