Theorem cbvalv1 2331

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1531  Ⅎwnf 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-11 2146  ax-12 2166

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-nf 1778

This theorem is referenced by:  cbvexv1  2332  cbval2v  2333  sb8fOLD  2344  sbbib  2351  cbvsbvf  2354  sb8eulem  2586  cbvmow  2591  abbib  2797  cleqh  2855  cleqf  2923  cbvralfw  3291  cbvralf  3343  ralab2  3689  cbvralcsf  3934  dfssf  3967  ab0OLD  4377  elintabOLD  4963  reusv2lem4  5401  cbviotaw  6508  cbviota  6511  sb8iota  6513  dffun6f  6567  findcard2  9189  findcard2OLD  9309  aceq1  10142  bnj1385  34594  sbcalf  37718  alrimii  37723  aomclem6  42625  rababg  43146