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

Theorem 19.41vv 1772
Description: Version of 19.41 1971 with two quantifiers and a dv condition requiring fewer axioms. (Contributed by NM, 30-Apr-1995.)
Assertion
Ref Expression
19.41vv
Distinct variable groups:   ,   ,

Proof of Theorem 19.41vv
StepHypRef Expression
1 19.41v 1771 . . 3
21exbii 1667 . 2
3 19.41v 1771 . 2
42, 3bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  E.wex 1612
This theorem is referenced by:  19.41vvv  1773  rabxp  5041  copsex2gb  5118  mpt2mptx  6393  xpassen  7631  dfac5lem1  8525  3v3e3cycl  24665  dfdm5  29206  dfrn5  29207  elima4  29209  brtxp2  29531  brpprod3a  29536  brimg  29587  brsuccf  29591  mpt2mptx2  32924  bnj996  34013  diblsmopel  36898
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