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

Theorem 19.42vv 1844
Description: Version of 19.42 2071 with two quantifiers and a dv condition requiring fewer axioms. (Contributed by NM, 16-Mar-1995.)
Assertion
Ref Expression
19.42vv  |-  ( E. x E. y (
ph  /\  ps )  <->  (
ph  /\  E. x E. y ps ) )
Distinct variable groups:    ph, x    ph, y
Allowed substitution hints:    ps( x, y)

Proof of Theorem 19.42vv
StepHypRef Expression
1 exdistr 1843 . 2  |-  ( E. x E. y (
ph  /\  ps )  <->  E. x ( ph  /\  E. y ps ) )
2 19.42v 1842 . 2  |-  ( E. x ( ph  /\  E. y ps )  <->  ( ph  /\ 
E. x E. y ps ) )
31, 2bitri 257 1  |-  ( E. x E. y (
ph  /\  ps )  <->  (
ph  /\  E. x E. y ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 376   E.wex 1671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813
This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672
This theorem is referenced by:  19.42vvv  1845  exdistr2  1846  3exdistr  1847  ceqsex3v  3074  ceqsex4v  3075  ceqsex8v  3077  elvvv  4899  xpdifid  5271  dfoprab2  6356  resoprab  6411  elrnmpt2res  6429  ov3  6452  ov6g  6453  oprabex3  6801  xpassen  7684  axaddf  9587  axmulf  9588  usgraedg4  25193  el2wlkonot  25676  el2spthonot  25677  el2wlkonotot0  25679  qqhval2  28860  bnj996  29838  dvhopellsm  34756
  Copyright terms: Public domain W3C validator