Theorem 19.37v 1989

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535  ∃wex 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965

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

This theorem is referenced by:  spc3egv  3603  eqvincg  3648  rmoanim  3903  rmoanimALT  3904  axrep5  5293  fvn0ssdmfun  7094  kmlem14  10202  kmlem15  10203  bnj132  34719  bnj1098  34776  bnj150  34869  bnj865  34916  bnj996  34949  bnj1021  34959  bnj1090  34972  bnj1176  34998  sn-axrep5v  42234  cnvssco  43596  refimssco  43597  19.37vv  44381  pm11.61  44389  relopabVD  44899