Theorem qimeqex-P7-L1 1054

Description: Lemma for qimeqex-P7 1056.

Assertion

Ref	Expression
qimeqex-P7-L1	⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑 → 𝜓))

Proof of Theorem qimeqex-P7-L1

Step	Hyp	Ref	Expression
1		ndnfrall1-P7.7 832	. . . . 5 ⊢ Ⅎ𝑥∀𝑥𝜑
2		ndnfrex1-P7.8 833	. . . . 5 ⊢ Ⅎ𝑥∃𝑥𝜓
3	1, 2	ndnfrim-P7.3.RC 876	. . . 4 ⊢ Ⅎ𝑥(∀𝑥𝜑 → ∃𝑥𝜓)
4	3, 1	ndnfrand-P7.4.RC 877	. . 3 ⊢ Ⅎ𝑥((∀𝑥𝜑 → ∃𝑥𝜓) ∧ ∀𝑥𝜑)
5		ndnfrex1-P7.8 833	. . 3 ⊢ Ⅎ𝑥∃𝑥(𝜑 → 𝜓)
6		rcp-NDASM2of2 194	. . . . . . 7 ⊢ (((∀𝑥𝜑 → ∃𝑥𝜓) ∧ 𝜓) → 𝜓)
7	6	axL1-P3.21 252	. . . . . 6 ⊢ (((∀𝑥𝜑 → ∃𝑥𝜓) ∧ 𝜓) → (𝜑 → 𝜓))
8	7	exi-P7 951	. . . . 5 ⊢ (((∀𝑥𝜑 → ∃𝑥𝜓) ∧ 𝜓) → ∃𝑥(𝜑 → 𝜓))
9	8	rcp-NDIMI2 224	. . . 4 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) → (𝜓 → ∃𝑥(𝜑 → 𝜓)))
10	9	rcp-NDIMP1add1 208	. . 3 ⊢ (((∀𝑥𝜑 → ∃𝑥𝜓) ∧ ∀𝑥𝜑) → (𝜓 → ∃𝑥(𝜑 → 𝜓)))
11		rcp-NDASM1of1 192	. . . 4 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
12	11	import-P3.34a.RC 306	. . 3 ⊢ (((∀𝑥𝜑 → ∃𝑥𝜓) ∧ ∀𝑥𝜑) → ∃𝑥𝜓)
13	4, 5, 10, 12	exe-P7 955	. 2 ⊢ (((∀𝑥𝜑 → ∃𝑥𝜓) ∧ ∀𝑥𝜑) → ∃𝑥(𝜑 → 𝜓))
14	1	ndnfrneg-P7.2.RC 875	. . . 4 ⊢ Ⅎ𝑥 ¬ ∀𝑥𝜑
15	3, 14	ndnfrand-P7.4.RC 877	. . 3 ⊢ Ⅎ𝑥((∀𝑥𝜑 → ∃𝑥𝜓) ∧ ¬ ∀𝑥𝜑)
16		rcp-NDASM2of2 194	. . . . . . . 8 ⊢ (((∀𝑥𝜑 → ∃𝑥𝜓) ∧ ¬ 𝜑) → ¬ 𝜑)
17	16	axL1-P3.21 252	. . . . . . 7 ⊢ (((∀𝑥𝜑 → ∃𝑥𝜓) ∧ ¬ 𝜑) → (¬ 𝜓 → ¬ 𝜑))
18	17	trnsp-P3.31d 288	. . . . . 6 ⊢ (((∀𝑥𝜑 → ∃𝑥𝜓) ∧ ¬ 𝜑) → (𝜑 → 𝜓))
19	18	exi-P7 951	. . . . 5 ⊢ (((∀𝑥𝜑 → ∃𝑥𝜓) ∧ ¬ 𝜑) → ∃𝑥(𝜑 → 𝜓))
20	19	rcp-NDIMI2 224	. . . 4 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) → (¬ 𝜑 → ∃𝑥(𝜑 → 𝜓)))
21	20	rcp-NDIMP1add1 208	. . 3 ⊢ (((∀𝑥𝜑 → ∃𝑥𝜓) ∧ ¬ ∀𝑥𝜑) → (¬ 𝜑 → ∃𝑥(𝜑 → 𝜓)))
22		rcp-NDASM2of2 194	. . . 4 ⊢ (((∀𝑥𝜑 → ∃𝑥𝜓) ∧ ¬ ∀𝑥𝜑) → ¬ ∀𝑥𝜑)
23		exnegall-P7 1046	. . . . 5 ⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
24	23	bisym-P3.33b.RC 299	. . . 4 ⊢ (¬ ∀𝑥𝜑 ↔ ∃𝑥 ¬ 𝜑)
25	22, 24	subimr2-P4.RC 543	. . 3 ⊢ (((∀𝑥𝜑 → ∃𝑥𝜓) ∧ ¬ ∀𝑥𝜑) → ∃𝑥 ¬ 𝜑)
26	15, 5, 21, 25	exe-P7 955	. 2 ⊢ (((∀𝑥𝜑 → ∃𝑥𝜓) ∧ ¬ ∀𝑥𝜑) → ∃𝑥(𝜑 → 𝜓))
27		ndexclmid-P3.16.AC 251	. 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) → (∀𝑥𝜑 ∨ ¬ ∀𝑥𝜑))
28	13, 26, 27	rcp-NDORE2 235	1 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑 → 𝜓))

Syntax hints:  ∀wff-forall 8  ¬ wff-neg 9   → wff-imp 10   ∧ wff-and 132  ∃wff-exists 595

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14  ax-GEN 15  ax-L4 16  ax-L5 17  ax-L6 18  ax-L7 19  ax-L10 27  ax-L11 28  ax-L12 29

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133  df-or-D2.3 145  df-true-D2.4 155  df-false-D2.5 158  df-rcp-AND3 161  df-exists-D5.1 596  df-nfree-D6.1 682  df-psub-D6.2 716

This theorem is referenced by:  qimeqex-P7  1056