Theorem 19.37v 2004

Description: Version of 19.37 2244 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 1884	. 2 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))
2		19.3v 1989	. . 3 ⊢ (∀𝑥𝜑 ↔ 𝜑)
3	2	imbi1i 350	. 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) ↔ (𝜑 → ∃𝑥𝜓))
4	1, 3	bitri 276	1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1545  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  spc3egv  3541  eqvincg  3586  rmoanim  3826  rmoanimALT  3827  axrep5  5207  fvn0ssdmfun  7015  kmlem14  10077  kmlem15  10078  bnj132  34909  bnj1098  34966  bnj150  35058  bnj865  35105  bnj996  35138  bnj1021  35148  bnj1090  35161  bnj1176  35187  sn-axrep5v  42704  cnvssco  44050  refimssco  44051  19.37vv  44829  pm11.61  44837  relopabVD  45344