Theorem cbvalv1 2347

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535  Ⅎwnf 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-nf 1782

This theorem is referenced by:  cbvexv1  2348  cbval2v  2349  sb8fOLD  2360  sbbib  2367  cbvsbvf  2369  sb8eulem  2601  cbvmow  2606  abbib  2814  cleqh  2874  cleqf  2940  cbvralfw  3310  cbvralf  3368  ralab2  3719  cbvralcsf  3966  dfssf  3999  ab0OLD  4403  elintabOLD  4983  reusv2lem4  5419  cbviotaw  6532  cbviota  6535  sb8iota  6537  dffun6f  6591  findcard2  9230  aceq1  10186  bnj1385  34808  sbcalf  38074  alrimii  38079  aomclem6  43016  rababg  43536