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

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

Proof of Theorem 19.42v
StepHypRef Expression
1 19.41v 1771 . 2
2 exancom 1671 . 2
3 ancom 450 . 2
41, 2, 33bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  E.wex 1612
This theorem is referenced by:  exdistr  1776  19.42vv  1777  19.42vvv  1778  4exdistr  1781  eeeanv  1989  cbvex2OLD  2029  2sb5  2187  rexcom4a  3130  ceqsex2  3147  reuind  3303  2reu5lem3  3307  sbccomlem  3406  bm1.3ii  4576  eqvinop  4736  dmopabss  5219  dmopab3  5220  mptpreima  5505  brprcneu  5864  fndmin  5994  fliftf  6213  dfoprab2  6343  dmoprab  6383  dmoprabss  6384  fnoprabg  6403  uniuni  6609  zfrep6  6768  opabex3d  6778  opabex3  6779  fsplit  6905  eroveu  7425  rankuni  8302  aceq1  8519  dfac3  8523  kmlem14  8564  kmlem15  8565  axdc2lem  8849  1idpr  9428  ltexprlem1  9435  ltexprlem4  9438  shftdm  12904  joindm  15633  meetdm  15647  ntreq0  19578  cnextf  20566  usg2spot2nb  25065  adjeu  26808  rexunirn  27390  mptfnf  27499  fpwrelmapffslem  27555  dfiota3  29573  brimg  29587  funpartlem  29592  itg2addnc  30069  sbccom2lem  30529  pm11.58  31296  pm11.71  31303  2sbc5g  31323  iotasbc2  31327  stoweidlem60  31842  ax6e2nd  33331  ax6e2ndVD  33708  ax6e2ndALT  33730  bnj1019  33838  bnj1209  33855  bnj1033  34025  bnj1189  34065  bj-eeanvw  34267  bj-rexcom4  34445  bj-rexcom4a  34446  bj-snsetex  34521  bj-snglc  34527  rp-isfinite6  37744  elintima  37765  xpcogend  37773
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