Theorem 19.35 1881

Description: Theorem 19.35 of [Margaris] p. 90. This theorem is useful for moving an implication (in the form of the right-hand side) into the scope of a single existential quantifier. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.)

Assertion

Ref	Expression
19.35	⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))

Proof of Theorem 19.35

Step	Hyp	Ref	Expression
1		pm2.27 42	. . . 4 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))
2	1	aleximi 1835	. . 3 ⊢ (∀𝑥𝜑 → (∃𝑥(𝜑 → 𝜓) → ∃𝑥𝜓))
3	2	com12 32	. 2 ⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
4		exnal 1830	. . . 4 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
5		pm2.21 123	. . . . 5 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
6	5	eximi 1838	. . . 4 ⊢ (∃𝑥 ¬ 𝜑 → ∃𝑥(𝜑 → 𝜓))
7	4, 6	sylbir 234	. . 3 ⊢ (¬ ∀𝑥𝜑 → ∃𝑥(𝜑 → 𝜓))
8		exa1 1841	. . 3 ⊢ (∃𝑥𝜓 → ∃𝑥(𝜑 → 𝜓))
9	7, 8	ja 186	. 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑 → 𝜓))
10	3, 9	impbii 208	1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205  ∀wal 1537  ∃wex 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813

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

This theorem is referenced by:  19.35i  1882  19.35ri  1883  19.25  1884  19.43  1886  nfimd  1898  19.36imvOLD  1950  19.37imv  1952  speimfwALT  1969  19.39  1989  19.24  1990  19.36v  1992  19.37v  1996  19.36  2226  19.37  2228  spimt  2386  grothprim  10521  bj-nfimt  34746  bj-nnfim  34855  bj-19.36im  34880  bj-19.37im  34881  bj-spimt2  34894  bj-spimtv  34903