Theorem cbvallv-P5 659

Description: Change of Bound Variable Law for '∀𝑥' (variable restriction).

'𝑥' cannot occur in '𝜓' and '𝑦' cannot occur in '𝜑'.

The hypothesis is fulfilled when every free occurrence of '𝑥' in '𝜑' is replaced with '𝑦', and every bound occurance of '𝑥' is replaced with a fresh variable (one for each quantifier). The resulting WFF is '𝜓'.

The most general form is cbvall-P6 751.

Hypothesis

Ref	Expression
cbvallv-P5.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvallv-P5	⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

Distinct variable groups:   𝜑,𝑦   𝜓,𝑥   𝑥,𝑦

Proof of Theorem cbvallv-P5

Step	Hyp	Ref	Expression
1		cbvallv-P5.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
2	1	ndbief-P3.14 179	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
3	2	cbvallv-P5-L1 658	. 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	cbvallv-P5-L1 658	. 2 ⊢ (∀𝑦𝜓 → ∀𝑥𝜑)
8	3, 7	rcp-NDBII0 239	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:  cbvexv-P5  660  specw-P5  661  example-E5.03a  665  lemma-L5.04a  667  example-E5.04a  675  genallw-P6  676  nfrall1w-P6  692  example-E6.01a  706  psubjust-P6  715  nfrterm-P6  779