Theorem 19.37v 1993

Description: Version of 19.37 2223 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 348	. 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) ↔ (𝜑 → ∃𝑥𝜓))
4	1, 3	bitri 274	1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969

This theorem depends on definitions:  df-bi 206  df-ex 1780

This theorem is referenced by:  spc3egv  3592  eqvincg  3635  rmoanim  3887  rmoanimALT  3888  axrep5  5290  fvn0ssdmfun  7075  kmlem14  10160  kmlem15  10161  bnj132  34035  bnj1098  34092  bnj150  34185  bnj865  34232  bnj996  34265  bnj1021  34275  bnj1090  34288  bnj1176  34314  sn-axrep5v  41339  cnvssco  42659  refimssco  42660  19.37vv  43446  pm11.61  43454  relopabVD  43964