Theorem cbvex-P6 752

Description: Change of Bound Variable Law for '∃𝑥' (non-freeness condition).

Hypotheses

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

Assertion

Ref	Expression
cbvex-P6	⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Distinct variable group:   𝑥,𝑦

Proof of Theorem cbvex-P6

Step	Hyp	Ref	Expression
1		df-exists-D5.1 596	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
2		cbvex-P6.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
3		nfrneg-P6 688	. . . . 5 ⊢ (Ⅎ𝑥 ¬ 𝜓 ↔ Ⅎ𝑥𝜓)
4	2, 3	bimpr-P4.RC 534	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓
5		cbvex-P6.2	. . . . 5 ⊢ Ⅎ𝑦𝜑
6		nfrneg-P6 688	. . . . 5 ⊢ (Ⅎ𝑦 ¬ 𝜑 ↔ Ⅎ𝑦𝜑)
7	5, 6	bimpr-P4.RC 534	. . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑
8		cbvex-P6.3	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
9	8	subneg-P3.39 323	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
10	4, 7, 9	cbvall-P6 751	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
11	10	subneg-P3.39.RC 324	. 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
12		df-exists-D5.1 596	. . 3 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
13	12	bisym-P3.33b.RC 299	. 2 ⊢ (¬ ∀𝑦 ¬ 𝜓 ↔ ∃𝑦𝜓)
14	1, 11, 13	dbitrns-P4.16.RC 429	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Syntax hints:  term-obj 1   = wff-equals 6  ∀wff-forall 8  ¬ wff-neg 9   → wff-imp 10   ↔ wff-bi 104  ∃wff-exists 595  Ⅎwff-nfree 681

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

This theorem is referenced by:  cbvexpsub-P6  769