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

Theorem 19.42vv 1958
 Description: Version of 19.42 2239 with two quantifiers and a disjoint variable condition requiring fewer axioms. (Contributed by NM, 16-Mar-1995.)
Assertion
Ref Expression
19.42vv (∃𝑥𝑦(𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝑦𝜓))
Distinct variable groups:   𝜑,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜓(𝑥,𝑦)

Proof of Theorem 19.42vv
StepHypRef Expression
1 exdistr 1955 . 2 (∃𝑥𝑦(𝜑𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2 19.42v 1954 . 2 (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥𝑦𝜓))
31, 2bitri 278 1 (∃𝑥𝑦(𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝑦𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399  ∃wex 1781 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782 This theorem is referenced by:  exdistr2  1959  19.42vvvOLD  1961  3exdistr  1962  ceqsex3v  3520  ceqsex4v  3521  ceqsex8v  3523  elvvv  5604  xpdifid  6003  dfoprab2  7196  resoprab  7254  elrnmpores  7272  ov3  7296  ov6g  7297  oprabex3  7664  xpassen  8598  axaddf  10556  axmulf  10557  qqhval2  31297  bnj996  32302  inxpxrn  35765  dvhopellsm  38375
 Copyright terms: Public domain W3C validator