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 1991
Description: Version of 19.37 2232 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 1877 . 2 (∃𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))
2 19.3v 1981 . . 3 (∀𝑥𝜑𝜑)
32imbi1i 349 . 2 ((∀𝑥𝜑 → ∃𝑥𝜓) ↔ (𝜑 → ∃𝑥𝜓))
41, 3bitri 275 1 (∃𝑥(𝜑𝜓) ↔ (𝜑 → ∃𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1538  wex 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967
This theorem depends on definitions:  df-bi 207  df-ex 1780
This theorem is referenced by:  spc3egv  3603  eqvincg  3648  rmoanim  3894  rmoanimALT  3895  axrep5  5287  fvn0ssdmfun  7094  kmlem14  10204  kmlem15  10205  bnj132  34740  bnj1098  34797  bnj150  34890  bnj865  34937  bnj996  34970  bnj1021  34980  bnj1090  34993  bnj1176  35019  sn-axrep5v  42255  cnvssco  43619  refimssco  43620  19.37vv  44404  pm11.61  44412  relopabVD  44921
  Copyright terms: Public domain W3C validator