Theorem 19.37v 1998

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

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  3553  eqvincg  3598  rmoanim  3840  rmoanimALT  3841  axrep5  5223  fvn0ssdmfun  7007  kmlem14  10055  kmlem15  10056  bnj132  34738  bnj1098  34795  bnj150  34888  bnj865  34935  bnj996  34968  bnj1021  34978  bnj1090  34991  bnj1176  35017  sn-axrep5v  42257  cnvssco  43647  refimssco  43648  19.37vv  44426  pm11.61  44434  relopabVD  44941