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

Theorem 19.23v 1760
Description: Version of 19.23 1910 with a dv condition instead of a non-freeness hypothesis. (Contributed by NM, 28-Jun-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 11-Jan-2020.)
Assertion
Ref Expression
19.23v
Distinct variable group:   ,

Proof of Theorem 19.23v
StepHypRef Expression
1 exim 1654 . . 3
2 19.9v 1754 . . 3
31, 2syl6ib 226 . 2
4 ax-5 1704 . . . 4
54imim2i 14 . . 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.23vv  1761  pm11.53v  1764  2mo2  2372  2eu4OLD  2381  euind  3286  reuind  3303  r19.3rzv  3922  unissb  4281  disjor  4436  dftr2  4547  ssrelrel  5108  cotrg  5383  dffun2  5603  fununi  5659  dff13  6166  dffi2  7903  aceq2  8521  psgnunilem4  16522  metcld  21744  metcld2  21745  isch2  26141  disjorf  27440  funcnv5mpt  27511  dfon2lem8  29222  pm10.52  31270  truniALT  33312  tpid3gVD  33642  truniALTVD  33678  onfrALTVD  33691  unisnALT  33726  bnj1052  34031  bnj1030  34043  bj-equsalvv  34310  elintima  37765  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  ax-6 1747
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator