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

Theorem 19.23v 1903
 Description: Special case of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jun-1998.)
Assertion
Ref Expression
19.23v
Distinct variable group:   ,
Allowed substitution hint:   ()

Proof of Theorem 19.23v
StepHypRef Expression
1 nfv 1626 . 2
2119.23 1809 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177  wal 1546  wex 1547 This theorem is referenced by:  19.23vv  1904  2eu4  2321  euind  3064  reuind  3080  r19.3rzv  3664  unissb  3987  disjor  4137  dftr2  4245  ssrelrel  4916  cotr  5186  dffun2  5404  fununi  5457  dff13  5943  dffi2  7363  aceq2  7933  metcld  19129  metcld2  19130  isch2  22574  disjorf  23865  funcnv5mpt  23925  dfon2lem8  25170  psgnunilem4  27089  pm10.52  27229  truniALT  27969  tpid3gVD  28295  truniALTVD  28331  onfrALTVD  28344  unisnALT  28379  bnj1052  28682  bnj1030  28694 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-11 1753 This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551
 Copyright terms: Public domain W3C validator