Theorem 19.37v 1998

Description: Version of 19.37 2239 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

Step	Hyp	Ref	Expression
1		19.35 1878	. 2 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))
2		19.3v 1983	. . 3 ⊢ (∀𝑥𝜑 ↔ 𝜑)
3	2	imbi1i 349	. 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) ↔ (𝜑 → ∃𝑥𝜓))
4	1, 3	bitri 275	1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968

This theorem depends on definitions:  df-bi 207  df-ex 1781

This theorem is referenced by:  spc3egv  3557  eqvincg  3602  rmoanim  3844  rmoanimALT  3845  axrep5  5232  fvn0ssdmfun  7019  kmlem14  10074  kmlem15  10075  bnj132  34882  bnj1098  34939  bnj150  35032  bnj865  35079  bnj996  35112  bnj1021  35122  bnj1090  35135  bnj1176  35161  sn-axrep5v  42473  cnvssco  43847  refimssco  43848  19.37vv  44626  pm11.61  44634  relopabVD  45141