Theorem 19.37v 2031

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001

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

This theorem is used by:  spc3egv  3560  eqvincg  3604  rmoanim  3845  rmoanimALT  3846  axrep5  5241  fvn0ssdmfun  7082  kmlem14  10252  kmlem15  10253  bnj132  35410  bnj1098  35467  bnj150  35559  bnj865  35606  bnj996  35639  bnj1021  35649  bnj1090  35662  bnj1176  35688  sn-axrep5v  43411  cnvssco  44746  refimssco  44747  19.37vv  45509  pm11.61  45517  relopabVD  46022