Theorem example-E6.02a 712

Description: Eliminating Hypothesis to solvedsub-P6a 711.

In this example we replace '𝑏' in 𝜑 with '(𝑥 ⋅ 𝑏)'. Because '𝑏' occurs in the term '(𝑥 ⋅ 𝑏)', we first replace '𝑏' with '𝑐' to obtain '𝜓'. Because '𝑥' is a bound variable in '𝜑', we again use cbvallv-P5 659 to change the bound variable '𝑥' to '𝑦' so as not to conflict with the substituted term, '(𝑥 ⋅ 𝑏)'. The WFF metavariables '𝜑', '𝜓', and '𝜒' defined as hypotheses, exist only to make this example easier to follow. It is easy to locate the important steps, which are...

'Ⅎ𝑏𝜓',

'Ⅎ𝑐𝜒,

'(𝑏 = 𝑐 → (𝜑 ↔ 𝜓))',

and '(𝑐 = (𝑥 ⋅ 𝑏)) → (𝜓 ↔ 𝜒))'.

Hypotheses

Ref	Expression
example-E6.02a.1	⊢ (𝑏 = 𝑏₁ → (𝜓 ↔ 𝜓₁))
example-E6.02a.2	⊢ (𝑐 = 𝑐₁ → (𝜒 ↔ 𝜒₁))
example-E6.02a.3	⊢ (𝜑 ↔ ∃𝑥 𝑏 = (𝑥 ⋅ 𝑎))
example-E6.02a.4	⊢ (𝜓 ↔ ∃𝑥 𝑐 = (𝑥 ⋅ 𝑎))
example-E6.02a.5	⊢ (𝜒 ↔ ∃𝑦 (𝑥 ⋅ 𝑏) = (𝑦 ⋅ 𝑎))

Assertion

Ref	Expression
example-E6.02a	⊢ (𝜒 ↔ ∀𝑐(𝑐 = (𝑥 ⋅ 𝑏) → ∀𝑏(𝑏 = 𝑐 → 𝜑)))

Distinct variable groups:   𝜓,𝑏₁   𝜓₁,𝑏   𝜒,𝑐₁   𝜒₁,𝑐   𝑎,𝑏,𝑏₁,𝑐,𝑐₁,𝑥,𝑦

Proof of Theorem example-E6.02a

Step	Hyp	Ref	Expression
1		example-E6.02a.1	. 2 ⊢ (𝑏 = 𝑏₁ → (𝜓 ↔ 𝜓₁))
2		nfrv-P6 686	. . 3 ⊢ Ⅎ𝑏∃𝑥 𝑐 = (𝑥 ⋅ 𝑎)
3		example-E6.02a.4	. . . . 5 ⊢ (𝜓 ↔ ∃𝑥 𝑐 = (𝑥 ⋅ 𝑎))
4	3	bisym-P3.33b.RC 299	. . . 4 ⊢ (∃𝑥 𝑐 = (𝑥 ⋅ 𝑎) ↔ 𝜓)
5	4	nfrleq-P6 687	. . 3 ⊢ (Ⅎ𝑏∃𝑥 𝑐 = (𝑥 ⋅ 𝑎) ↔ Ⅎ𝑏𝜓)
6	2, 5	bimpf-P4.RC 532	. 2 ⊢ Ⅎ𝑏𝜓
7		example-E6.02a.2	. 2 ⊢ (𝑐 = 𝑐₁ → (𝜒 ↔ 𝜒₁))
8		nfrv-P6 686	. . 3 ⊢ Ⅎ𝑐∃𝑦 (𝑥 ⋅ 𝑏) = (𝑦 ⋅ 𝑎)
9		example-E6.02a.5	. . . . 5 ⊢ (𝜒 ↔ ∃𝑦 (𝑥 ⋅ 𝑏) = (𝑦 ⋅ 𝑎))
10	9	bisym-P3.33b.RC 299	. . . 4 ⊢ (∃𝑦 (𝑥 ⋅ 𝑏) = (𝑦 ⋅ 𝑎) ↔ 𝜒)
11	10	nfrleq-P6 687	. . 3 ⊢ (Ⅎ𝑐∃𝑦 (𝑥 ⋅ 𝑏) = (𝑦 ⋅ 𝑎) ↔ Ⅎ𝑐𝜒)
12	8, 11	bimpf-P4.RC 532	. 2 ⊢ Ⅎ𝑐𝜒
13		subeql-P5.CL 633	. . . 4 ⊢ (𝑏 = 𝑐 → (𝑏 = (𝑥 ⋅ 𝑎) ↔ 𝑐 = (𝑥 ⋅ 𝑎)))
14	13	subexv-P5 624	. . 3 ⊢ (𝑏 = 𝑐 → (∃𝑥 𝑏 = (𝑥 ⋅ 𝑎) ↔ ∃𝑥 𝑐 = (𝑥 ⋅ 𝑎)))
15		example-E6.02a.3	. . . . 5 ⊢ (𝜑 ↔ ∃𝑥 𝑏 = (𝑥 ⋅ 𝑎))
16	15	bisym-P3.33b.RC 299	. . . 4 ⊢ (∃𝑥 𝑏 = (𝑥 ⋅ 𝑎) ↔ 𝜑)
17	16, 4	subbid-P3.41c.RC 337	. . 3 ⊢ ((∃𝑥 𝑏 = (𝑥 ⋅ 𝑎) ↔ ∃𝑥 𝑐 = (𝑥 ⋅ 𝑎)) ↔ (𝜑 ↔ 𝜓))
18	14, 17	subimr2-P4.RC 543	. 2 ⊢ (𝑏 = 𝑐 → (𝜑 ↔ 𝜓))
19		ax-L9-multl 25	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 ⋅ 𝑎) = (𝑦 ⋅ 𝑎))
20	19	subeqr-P5 635	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑐 = (𝑥 ⋅ 𝑎) ↔ 𝑐 = (𝑦 ⋅ 𝑎)))
21	20	cbvexv-P5 660	. . . . 5 ⊢ (∃𝑥 𝑐 = (𝑥 ⋅ 𝑎) ↔ ∃𝑦 𝑐 = (𝑦 ⋅ 𝑎))
22	21	rcp-NDIMP0addall 207	. . . 4 ⊢ (𝑐 = (𝑥 ⋅ 𝑏) → (∃𝑥 𝑐 = (𝑥 ⋅ 𝑎) ↔ ∃𝑦 𝑐 = (𝑦 ⋅ 𝑎)))
23		subeql-P5.CL 633	. . . . 5 ⊢ (𝑐 = (𝑥 ⋅ 𝑏) → (𝑐 = (𝑦 ⋅ 𝑎) ↔ (𝑥 ⋅ 𝑏) = (𝑦 ⋅ 𝑎)))
24	23	subexv-P5 624	. . . 4 ⊢ (𝑐 = (𝑥 ⋅ 𝑏) → (∃𝑦 𝑐 = (𝑦 ⋅ 𝑎) ↔ ∃𝑦 (𝑥 ⋅ 𝑏) = (𝑦 ⋅ 𝑎)))
25	22, 24	bitrns-P3.33c 302	. . 3 ⊢ (𝑐 = (𝑥 ⋅ 𝑏) → (∃𝑥 𝑐 = (𝑥 ⋅ 𝑎) ↔ ∃𝑦 (𝑥 ⋅ 𝑏) = (𝑦 ⋅ 𝑎)))
26	4, 10	subbid-P3.41c.RC 337	. . 3 ⊢ ((∃𝑥 𝑐 = (𝑥 ⋅ 𝑎) ↔ ∃𝑦 (𝑥 ⋅ 𝑏) = (𝑦 ⋅ 𝑎)) ↔ (𝜓 ↔ 𝜒))
27	25, 26	subimr2-P4.RC 543	. 2 ⊢ (𝑐 = (𝑥 ⋅ 𝑏) → (𝜓 ↔ 𝜒))
28	1, 6, 7, 12, 18, 27	solvedsub-P6a 711	1 ⊢ (𝜒 ↔ ∀𝑐(𝑐 = (𝑥 ⋅ 𝑏) → ∀𝑏(𝑏 = 𝑐 → 𝜑)))

Syntax hints:  term-obj 1   ⋅ term-mult 5   = wff-equals 6  ∀wff-forall 8   → 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-L9-multl 25

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: (None)