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

Theorem 19.41v 1771
Description: Version of 19.41 1971 with a dv condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
19.41v
Distinct variable group:   ,

Proof of Theorem 19.41v
StepHypRef Expression
1 19.40 1679 . . 3
2 19.9v 1754 . . . 4
32anbi2i 694 . . 3
41, 3sylib 196 . 2
5 pm3.21 448 . . . 4
65eximdv 1710 . . 3
76impcom 430 . 2
84, 7impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  E.wex 1612
This theorem is referenced by:  19.41vv  1772  19.41vvv  1773  19.41vvvv  1774  19.42v  1775  r19.41v  3009  gencbvex  3153  euxfr  3285  euind  3286  zfpair  4689  opabn0  4783  eliunxp  5145  relop  5158  dmuni  5217  dmres  5299  dminss  5425  imainss  5426  ssrnres  5450  cnvresima  5501  resco  5516  rnco  5518  coass  5531  xpco  5552  rnoprab  6385  f11o  6762  frxp  6910  omeu  7253  domen  7549  xpassen  7631  kmlem3  8553  cflem  8647  genpass  9408  ltexprlem4  9438  hasheqf1oi  12424  3v3e3cycl2  24664  dftr6  29179  prter2  30622  pm11.6  31298  pm11.71  31303  rfcnnnub  31411  eliunxp2  32923  bnj534  33795  bnj906  33988  bnj908  33989  bnj916  33991  bnj983  34009  bnj986  34012  bj-eeanvw  34267  bj-csbsnlem  34470  bj-ccinftydisj  34616  dihglb2  37069
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-an 371  df-ex 1613
  Copyright terms: Public domain W3C validator