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

Theorem 19.42vv 1777
Description: Version of 19.42 1972 with two quantifiers and a dv condition requiring fewer axioms. (Contributed by NM, 16-Mar-1995.)
Assertion
Ref Expression
19.42vv
Distinct variable groups:   ,   ,

Proof of Theorem 19.42vv
StepHypRef Expression
1 exdistr 1776 . 2
2 19.42v 1775 . 2
31, 2bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  E.wex 1612
This theorem is referenced by:  19.42vvv  1778  exdistr2  1779  3exdistr  1780  ceqsex3v  3149  ceqsex4v  3150  ceqsex8v  3152  elvvv  5064  xpdifid  5440  dfoprab2  6343  resoprab  6398  elrnmpt2res  6416  ov3  6439  ov6g  6440  oprabex3  6789  xpassen  7631  axaddf  9543  axmulf  9544  usgraedg4  24387  el2wlkonot  24869  el2spthonot  24870  el2wlkonotot0  24872  qqhval2  27963  bnj996  34013  dvhopellsm  36844
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