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

Theorem 19.37v 1987
Description: Version of 19.37 2220 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
19.37v (∃𝑥(𝜑𝜓) ↔ (𝜑 → ∃𝑥𝜓))
Distinct variable group:   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem 19.37v
StepHypRef Expression
1 19.35 1872 . 2 (∃𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))
2 19.3v 1977 . . 3 (∀𝑥𝜑𝜑)
32imbi1i 348 . 2 ((∀𝑥𝜑 → ∃𝑥𝜓) ↔ (𝜑 → ∃𝑥𝜓))
41, 3bitri 274 1 (∃𝑥(𝜑𝜓) ↔ (𝜑 → ∃𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1531  wex 1773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963
This theorem depends on definitions:  df-bi 206  df-ex 1774
This theorem is referenced by:  spc3egv  3592  eqvincg  3636  rmoanim  3889  rmoanimALT  3890  axrep5  5295  fvn0ssdmfun  7089  kmlem14  10194  kmlem15  10195  bnj132  34390  bnj1098  34447  bnj150  34540  bnj865  34587  bnj996  34620  bnj1021  34630  bnj1090  34643  bnj1176  34669  sn-axrep5v  41735  cnvssco  43067  refimssco  43068  19.37vv  43853  pm11.61  43861  relopabVD  44371
  Copyright terms: Public domain W3C validator