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

Theorem 19.37v 1999
 Description: Version of 19.37 2235 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 1879 . 2 (∃𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))
2 19.3v 1987 . . 3 (∀𝑥𝜑𝜑)
32imbi1i 353 . 2 ((∀𝑥𝜑 → ∃𝑥𝜓) ↔ (𝜑 → ∃𝑥𝜓))
41, 3bitri 278 1 (∃𝑥(𝜑𝜓) ↔ (𝜑 → ∃𝑥𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536  ∃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 1912  ax-6 1971 This theorem depends on definitions:  df-bi 210  df-ex 1782 This theorem is referenced by:  spc3egv  3581  eqvincg  3618  rmoanim  3852  rmoanimALT  3853  axrep5  5169  fvn0ssdmfun  6815  kmlem14  9566  kmlem15  9567  bnj132  32004  bnj1098  32063  bnj150  32156  bnj865  32203  bnj996  32236  bnj1021  32246  bnj1090  32259  bnj1176  32285  sn-axrep5v  39238  cnvssco  40117  refimssco  40118  19.37vv  40904  pm11.61  40912  relopabVD  41422
 Copyright terms: Public domain W3C validator