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 2096
Description: Version of 19.37 2275 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 1980 . 2 (∃𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))
2 19.3v 2085 . . 3 (∀𝑥𝜑𝜑)
32imbi1i 341 . 2 ((∀𝑥𝜑 → ∃𝑥𝜓) ↔ (𝜑 → ∃𝑥𝜓))
41, 3bitri 267 1 (∃𝑥(𝜑𝜓) ↔ (𝜑 → ∃𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wal 1654  wex 1878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075
This theorem depends on definitions:  df-bi 199  df-ex 1879
This theorem is referenced by:  19.37ivOLD  2097  eqvincg  3547  axrep5  5002  fvn0ssdmfun  6604  kmlem14  9307  kmlem15  9308  bnj132  31337  bnj1098  31396  bnj150  31488  bnj865  31535  bnj996  31567  bnj1021  31576  bnj1090  31589  bnj1176  31615  bj-axrep5  33316  cnvssco  38752  refimssco  38753  19.37vv  39423  pm11.61  39432  relopabVD  39954  rmoanim  42002
  Copyright terms: Public domain W3C validator