Theorem cbvalv1 2340

Description: Rule used to change bound variables, using implicit substitution. Version of cbval 2398 with a disjoint variable condition, which does not require ax-13 2372. See cbvalvw 2040 for a version with two more disjoint variable conditions, requiring fewer axioms, and cbvalv 2400 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 228	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
5	1, 2, 4	cbv3v 2334	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
6	3	biimprd 247	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜓 → 𝜑))
7	6	equcoms 2024	. . 3 ⊢ (𝑦 = 𝑥 → (𝜓 → 𝜑))
8	2, 1, 7	cbv3v 2334	. 2 ⊢ (∀𝑦𝜓 → ∀𝑥𝜑)
9	5, 8	impbii 208	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537  Ⅎwnf 1787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-11 2156  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-nf 1788

This theorem is referenced by:  cbvexv1  2341  cbval2v  2342  cbval2vOLD  2343  sb8v  2352  sbbib  2359  sbievg  2361  sb8eulem  2598  cbvmow  2603  abbi  2811  cleqh  2862  cleqf  2937  cbvralfw  3358  cbvralfwOLD  3359  cbvralf  3361  ralab2  3627  ralab2OLD  3628  cbvralcsf  3873  dfss2f  3907  ab0OLD  4306  elintab  4887  reusv2lem4  5319  cbviotaw  6383  cbviota  6386  sb8iota  6388  dffun6f  6432  findcard2  8909  findcard2OLD  8986  aceq1  9804  bnj1385  32712  sbcalf  36199  alrimii  36204  aomclem6  40800  rababg  41070