Theorem specw-P5 661

Description: Weak Version of Law of Specialization.

Note that the hypothesis only requires the existence of a dummy variable '𝑥₁' and dummy formula '𝜑₁', that is equivalent to '𝜑' with free occurences of '𝑥' replaced with '𝑥₁' and bound occurances of '𝑥' replaced with fresh variables. Using induction on formula length, one can prove a meta-theorem stating that such a formula always exists. The building blocks of the inductive proof are the substitution theorems (theorems beginning with "sub") and the two bound variable replacement theorems (cbvallv-P5 659 and cbvexv-P5 660).

Because meta-theorems don't exist in metamath, we will need the auxiliary "scheme completeness" axiom ax-L12 29 to eliminate the hypothesis in the general case (see spec-P6 719).

Hypothesis

Ref	Expression
specw-P5.1	⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))

Assertion

Ref	Expression
specw-P5	⊢ (∀𝑥𝜑 → 𝜑)

Distinct variable groups:   𝜑,𝑥₁   𝜑₁,𝑥   𝑥,𝑥₁

Proof of Theorem specw-P5

Step	Hyp	Ref	Expression
1		specw-P5.1	. . . 4 ⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))
2	1	cbvallv-P5 659	. . 3 ⊢ (∀𝑥𝜑 ↔ ∀𝑥₁𝜑₁)
3	2	rcp-NDBIEF0 240	. 2 ⊢ (∀𝑥𝜑 → ∀𝑥₁𝜑₁)
4	1	ndbier-P3.15 180	. . . 4 ⊢ (𝑥 = 𝑥₁ → (𝜑₁ → 𝜑))
5		eqsym-P5.CL.SYM 629	. . . 4 ⊢ (𝑥 = 𝑥₁ ↔ 𝑥₁ = 𝑥)
6	4, 5	subiml2-P4.RC 541	. . 3 ⊢ (𝑥₁ = 𝑥 → (𝜑₁ → 𝜑))
7	6	lemma-L5.02a 653	. 2 ⊢ (∀𝑥₁𝜑₁ → 𝜑)
8	3, 7	syl-P3.24.RC 260	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:  term-obj 1   = wff-equals 6  ∀wff-forall 8   → wff-imp 10   ↔ wff-bi 104

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

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

This theorem is referenced by:  exiw-P5  662  qremallw-P6  702