Theorem 19.37v 1999

Description: Version of 19.37 2240 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 1879	. 2 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))
2		19.3v 1984	. . 3 ⊢ (∀𝑥𝜑 ↔ 𝜑)
3	2	imbi1i 349	. 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) ↔ (𝜑 → ∃𝑥𝜓))
4	1, 3	bitri 275	1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540  ∃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 1969

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

This theorem is referenced by:  spc3egv  3545  eqvincg  3590  rmoanim  3832  rmoanimALT  3833  axrep5  5220  fvn0ssdmfun  7026  kmlem14  10086  kmlem15  10087  bnj132  34869  bnj1098  34926  bnj150  35018  bnj865  35065  bnj996  35098  bnj1021  35108  bnj1090  35121  bnj1176  35147  sn-axrep5v  42658  cnvssco  44033  refimssco  44034  19.37vv  44812  pm11.61  44820  relopabVD  45327