Theorem example-E6.01a 706

Description: Eliminating Hypothesis to solvesub-P6a 704.

In this example we replace '𝑏' in 𝜑 with '𝑥'. Because '𝑥' is a bound variable in '𝜑', we use cbvallv-P5 659 to change the bound variable '𝑥' to '𝑦' so as not to conflict with the substituted '𝑥'. 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.01a.1	⊢ (𝑏 = 𝑏₁ → (𝜓 ↔ 𝜓₁))
example-E6.01a.2	⊢ (𝜑 ↔ ∀𝑥(𝑥 ∈ 𝑏 → 𝑥 ∈ 𝑎))
example-E6.01a.3	⊢ (𝜓 ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑎))

Assertion

Ref	Expression
example-E6.01a	⊢ (𝜓 ↔ ∀𝑏(𝑏 = 𝑥 → 𝜑))

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

Proof of Theorem example-E6.01a

Step	Hyp	Ref	Expression
1		example-E6.01a.1	. 2 ⊢ (𝑏 = 𝑏₁ → (𝜓 ↔ 𝜓₁))
2		nfrv-P6 686	. . 3 ⊢ Ⅎ𝑏∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑎)
3		example-E6.01a.3	. . . . 5 ⊢ (𝜓 ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑎))
4	3	bisym-P3.33b.RC 299	. . . 4 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑎) ↔ 𝜓)
5	4	nfrleq-P6 687	. . 3 ⊢ (Ⅎ𝑏∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑎) ↔ Ⅎ𝑏𝜓)
6	2, 5	bimpf-P4.RC 532	. 2 ⊢ Ⅎ𝑏𝜓
7		subelofl-P5.CL 639	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑏 ↔ 𝑦 ∈ 𝑏))
8		subelofl-P5.CL 639	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑎 ↔ 𝑦 ∈ 𝑎))
9	7, 8	subimd-P3.40c 329	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑏 → 𝑥 ∈ 𝑎) ↔ (𝑦 ∈ 𝑏 → 𝑦 ∈ 𝑎)))
10	9	cbvallv-P5 659	. . . . 5 ⊢ (∀𝑥(𝑥 ∈ 𝑏 → 𝑥 ∈ 𝑎) ↔ ∀𝑦(𝑦 ∈ 𝑏 → 𝑦 ∈ 𝑎))
11	10	rcp-NDIMP0addall 207	. . . 4 ⊢ (𝑏 = 𝑥 → (∀𝑥(𝑥 ∈ 𝑏 → 𝑥 ∈ 𝑎) ↔ ∀𝑦(𝑦 ∈ 𝑏 → 𝑦 ∈ 𝑎)))
12		subelofr-P5.CL 641	. . . . . 6 ⊢ (𝑏 = 𝑥 → (𝑦 ∈ 𝑏 ↔ 𝑦 ∈ 𝑥))
13	12	subiml-P3.40a 325	. . . . 5 ⊢ (𝑏 = 𝑥 → ((𝑦 ∈ 𝑏 → 𝑦 ∈ 𝑎) ↔ (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑎)))
14	13	suballv-P5 623	. . . 4 ⊢ (𝑏 = 𝑥 → (∀𝑦(𝑦 ∈ 𝑏 → 𝑦 ∈ 𝑎) ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑎)))
15	11, 14	bitrns-P3.33c 302	. . 3 ⊢ (𝑏 = 𝑥 → (∀𝑥(𝑥 ∈ 𝑏 → 𝑥 ∈ 𝑎) ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑎)))
16		example-E6.01a.2	. . . . 5 ⊢ (𝜑 ↔ ∀𝑥(𝑥 ∈ 𝑏 → 𝑥 ∈ 𝑎))
17	16	bisym-P3.33b.RC 299	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝑏 → 𝑥 ∈ 𝑎) ↔ 𝜑)
18	17, 4	subbid-P3.41c.RC 337	. . 3 ⊢ ((∀𝑥(𝑥 ∈ 𝑏 → 𝑥 ∈ 𝑎) ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑎)) ↔ (𝜑 ↔ 𝜓))
19	15, 18	subimr2-P4.RC 543	. 2 ⊢ (𝑏 = 𝑥 → (𝜑 ↔ 𝜓))
20	1, 6, 19	solvesub-P6a 704	1 ⊢ (𝜓 ↔ ∀𝑏(𝑏 = 𝑥 → 𝜑))

Syntax hints:  term-obj 1   = wff-equals 6   ∈ wff-elemof 7  ∀wff-forall 8   → wff-imp 10   ↔ wff-bi 104  Ⅎ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-L8-inl 20  ax-L8-inr 21

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)