Theorem 19.35 1878

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 1833	. . 3 ⊢ (∀𝑥𝜑 → (∃𝑥(𝜑 → 𝜓) → ∃𝑥𝜓))
3	2	com12 32	. 2 ⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
4		exnal 1828	. . . 4 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
5		pm2.21 123	. . . . 5 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
6	5	eximi 1836	. . . 4 ⊢ (∃𝑥 ¬ 𝜑 → ∃𝑥(𝜑 → 𝜓))
7	4, 6	sylbir 238	. . 3 ⊢ (¬ ∀𝑥𝜑 → ∃𝑥(𝜑 → 𝜓))
8		exa1 1839	. . 3 ⊢ (∃𝑥𝜓 → ∃𝑥(𝜑 → 𝜓))
9	7, 8	ja 189	. 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑 → 𝜓))
10	3, 9	impbii 212	1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1536  ∃wex 1781

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

This theorem depends on definitions:  df-bi 210  df-ex 1782

This theorem is referenced by:  19.35i  1879  19.35ri  1880  19.25  1881  19.43  1883  nfimd  1895  19.36imv  1946  19.37imv  1948  speimfwALT  1967  19.39  1991  19.24  1992  19.36v  1994  19.37v  1998  19.36  2230  19.37  2232  spimt  2393  grothprim  10245  bj-nfimt  34084  bj-nnfim  34190  bj-19.36im  34215  bj-19.37im  34216  bj-spimt2  34222  bj-spimtv  34231