Theorem 19.37v 1998

Description: Version of 19.37 2234 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 1986	. . 3 ⊢ (∀𝑥𝜑 ↔ 𝜑)
3	2	imbi1i 352	. 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) ↔ (𝜑 → ∃𝑥𝜓))
4	1, 3	bitri 277	1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1535  ∃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 1970

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

This theorem is referenced by:  spc3egv  3606  eqvincg  3643  rmoanim  3880  rmoanimALT  3881  axrep5  5198  fvn0ssdmfun  6844  kmlem14  9591  kmlem15  9592  bnj132  31998  bnj1098  32057  bnj150  32150  bnj865  32197  bnj996  32230  bnj1021  32240  bnj1090  32253  bnj1176  32279  sn-axrep5v  39115  cnvssco  39973  refimssco  39974  19.37vv  40724  pm11.61  40732  relopabVD  41242