Theorem specisub-P5 654

Description: Specialization Theorem with Implicit Substitution.

'𝑥' cannot occur in either '𝑡' or '𝜓'.

The hypothesis is fulfilled when every free occurence of '𝑥' in '𝜑' is replaced with the term '𝑡', and every bound occurence of '𝑥' is replaced with a fresh variable (one for each quantifier). The resulting WFF is '𝜓'. After this operation, '𝑥' will not occur in '𝜓'. '𝑥' cannot occur in '𝑡' either, or it would occur in '𝜓' wherever '𝑥' was replaced.

Hypothesis

Ref	Expression
specisub-P5.1	⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
specisub-P5	⊢ (∀𝑥𝜑 → 𝜓)

Distinct variable groups:   𝜓,𝑥   𝑡,𝑥

Proof of Theorem specisub-P5

Step	Hyp	Ref	Expression
1		specisub-P5.1	. . 3 ⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓))
2	1	ndbief-P3.14 179	. 2 ⊢ (𝑥 = 𝑡 → (𝜑 → 𝜓))
3	2	lemma-L5.02a 653	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

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:  exiisub-P5  655  qremallv-P5  656  lemma-L5.04a  667