Theorem cbvalv1 2338

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 2039 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 2332	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
6	3	biimprd 247	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜓 → 𝜑))
7	6	equcoms 2023	. . 3 ⊢ (𝑦 = 𝑥 → (𝜓 → 𝜑))
8	2, 1, 7	cbv3v 2332	. 2 ⊢ (∀𝑦𝜓 → ∀𝑥𝜑)
9	5, 8	impbii 208	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-11 2154  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-nf 1787

This theorem is referenced by:  cbvexv1  2339  cbval2v  2340  cbval2vOLD  2341  sb8fOLD  2352  sbbib  2359  sbievg  2361  sb8eulem  2598  cbvmow  2603  abbi  2810  cleqh  2862  cleqf  2938  cbvralfw  3368  cbvralfwOLD  3369  cbvralf  3371  ralab2  3634  cbvralcsf  3877  dfss2f  3911  ab0OLD  4309  elintab  4890  reusv2lem4  5324  cbviotaw  6398  cbviota  6401  sb8iota  6403  dffun6f  6448  findcard2  8947  findcard2OLD  9056  aceq1  9873  bnj1385  32812  sbcalf  36272  alrimii  36277  aomclem6  40884  rababg  41181