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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1540  Ⅎ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 1914  ax-6 1972  ax-7 2012  ax-11 2155  ax-12 2172

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

This theorem is referenced by:  cbvexv1  2339  cbval2v  2340  sb8fOLD  2351  sbbib  2358  cbvsbvf  2361  sb8eulem  2593  cbvmow  2598  abbib  2805  cleqh  2864  cleqf  2935  cbvralfw  3302  cbvralfwOLD  3321  cbvralf  3357  ralab2  3694  cbvralcsf  3939  dfss2f  3973  ab0OLD  4376  elintabOLD  4964  reusv2lem4  5400  cbviotaw  6503  cbviota  6506  sb8iota  6508  dffun6f  6562  findcard2  9164  findcard2OLD  9284  aceq1  10112  bnj1385  33843  sbcalf  36982  alrimii  36987  aomclem6  41801  rababg  42325