Theorem 19.37v 2032

Description: Version of 19.37 2272 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 1912	. 2 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))
2		19.3v 2017	. . 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 1945  ax-6 2002

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

This theorem is used by:  spc3egv  3561  eqvincg  3605  rmoanim  3846  rmoanimALT  3847  axrep5  5245  fvn0ssdmfun  7106  kmlem14  10281  kmlem15  10282  bnj132  35468  bnj1098  35525  bnj150  35617  bnj865  35664  bnj996  35697  bnj1021  35707  bnj1090  35720  bnj1176  35746  cbvex2ivw  43529  sn-axrep5v  43538  cnvssco  44867  refimssco  44868  19.37vv  45630  pm11.61  45638  relopabVD  46143