Theorem 19.37v 2030

Description: Version of 19.37 2268 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 1910	. 2 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))
2		19.3v 2015	. . 3 ⊢ (∀𝑥𝜑 ↔ 𝜑)
3	2	imbi1i 352	. 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) ↔ (𝜑 → ∃𝑥𝜓))
4	1, 3	bitri 278	1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  spc3egv  3557  eqvincg  3602  rmoanim  3842  rmoanimALT  3843  axrep5  5240  fvn0ssdmfun  7068  kmlem14  10169  kmlem15  10170  bnj132  35239  bnj1098  35296  bnj150  35388  bnj865  35435  bnj996  35468  bnj1021  35478  bnj1090  35491  bnj1176  35517  sn-axrep5v  43090  cnvssco  44449  refimssco  44450  19.37vv  45212  pm11.61  45220  relopabVD  45726