Theorem cbvalv1 2371

Description: Rule used to change bound variables, using implicit substitution. Version of cbval 2428 with a disjoint variable condition, which does not require ax-13 2402. See cbvalvw 2055 for a version with two more disjoint variable conditions, requiring fewer axioms, and cbvalv 2430 for another variant. (Contributed by NM, 13-May-1993.) (Revised by BJ, 31-May-2019.)

Hypotheses

Ref	Expression
cbvalv1.nf1	⊢ Ⅎ𝑦𝜑
cbvalv1.nf2	⊢ Ⅎ𝑥𝜓
cbvalv1.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvalv1	⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem cbvalv1

Step	Hyp	Ref	Expression
1		cbvalv1.nf1	. . 3 ⊢ Ⅎ𝑦𝜑
2		cbvalv1.nf2	. . 3 ⊢ Ⅎ𝑥𝜓
3		cbvalv1.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	3	biimpd 231	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
5	1, 2, 4	cbv3v 2365	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
6	3	biimprd 250	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜓 → 𝜑))
7	6	equcoms 2039	. . 3 ⊢ (𝑦 = 𝑥 → (𝜓 → 𝜑))
8	2, 1, 7	cbv3v 2365	. 2 ⊢ (∀𝑦𝜓 → ∀𝑥𝜑)
9	5, 8	impbii 211	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1557  Ⅎwnf 1802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-11 2190  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-nf 1803

This theorem is referenced by:  cbvexv1  2372  cbval2v  2373  sbbib  2391  cbvsbvf  2393  sb8eulem  2624  cbvmow  2629  abbib  2830  cleqh  2890  cleqf  2951  cbvralfw  3301  cbvralf  3346  ralab2  3658  cbvralcsf  3892  dfssf  3925  reusv2lem4  5355  cbviotaw  6478  cbviota  6480  sb8iota  6482  dffun6f  6530  findcard2  9126  aceq1  10066  bnj1385  35087  regsfromsetind  36859  bj-axseprep  37519  sbcalf  38573  alrimii  38578  aomclem6  43596  rababg  44110