Theorem cbvalv1 2350

Description: Rule used to change bound variables, using implicit substitution. Version of cbval 2405 with a disjoint variable condition, which does not require ax-13 2379. See cbvalvw 2043 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvalv 2407 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 232	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
5	1, 2, 4	cbv3v 2344	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
6	3	biimprd 251	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜓 → 𝜑))
7	6	equcoms 2027	. . 3 ⊢ (𝑦 = 𝑥 → (𝜓 → 𝜑))
8	2, 1, 7	cbv3v 2344	. 2 ⊢ (∀𝑦𝜓 → ∀𝑥𝜑)
9	5, 8	impbii 212	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-11 2158  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786

This theorem is referenced by:  cbvexv1  2351  cbval2v  2352  cbval2vOLD  2353  sb8v  2362  sbbib  2369  sb8eulem  2659  cbvmow  2663  abbi  2865  cbvabw  2867  cleqh  2913  cleqf  2983  cbvralfw  3382  cbvralfwOLD  3383  cbvralf  3385  ralab2  3636  ralab2OLD  3637  cbvralcsf  3870  dfss2f  3905  elintab  4849  reusv2lem4  5267  cbviotaw  6290  cbviota  6292  sb8iota  6294  dffun6f  6338  findcard2  8742  aceq1  9528  bnj1385  32214  sbcalf  35552  alrimii  35557  aomclem6  40003  rababg  40273