Theorem cbvex-P7-L1 1065

Description: Lemma for cbvex-P7 1066. †

Hypotheses

Ref	Expression
cbvex-P7-L1.1	⊢ Ⅎ𝑥𝜓
cbvex-P7-L1.2	⊢ Ⅎ𝑦𝜑
cbvex-P7-L1.3	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvex-P7-L1	⊢ (∃𝑦𝜓 → ∃𝑥𝜑)

Distinct variable group:   𝑥,𝑦

Proof of Theorem cbvex-P7-L1

Step	Hyp	Ref	Expression
1		cbvex-P7-L1.2	. . 3 ⊢ Ⅎ𝑦𝜑
2	1	ndnfrex2-P7.10.RC 881	. 2 ⊢ Ⅎ𝑦∃𝑥𝜑
3		cbvex-P7-L1.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
4		cbvex-P7-L1.3	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
5	3, 4	ndpsub1-P7.13 838	. . . 4 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
6	5	rcp-NDBIER0 241	. . 3 ⊢ (𝜓 → [𝑦 / 𝑥]𝜑)
7		ndexi-P7.19.CL 910	. . 3 ⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥𝜑)
8	6, 7	syl-P3.24.RC 260	. 2 ⊢ (𝜓 → ∃𝑥𝜑)
9	2, 8	exia-P7.RC 954	1 ⊢ (∃𝑦𝜓 → ∃𝑥𝜑)

Syntax hints:  term-obj 1   = wff-equals 6   → wff-imp 10   ↔ wff-bi 104  ∃wff-exists 595  Ⅎwff-nfree 681  [wff-psub 714

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-rcp-AND3 161  df-exists-D5.1 596  df-nfree-D6.1 682  df-psub-D6.2 716

This theorem is referenced by:  cbvex-P7  1066