Theorem cbvalv1 2346

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540  Ⅎ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 1912  ax-6 1969  ax-7 2010  ax-11 2163  ax-12 2185

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

This theorem is referenced by:  cbvexv1  2347  cbval2v  2348  sbbib  2366  cbvsbvf  2368  sb8eulem  2599  cbvmow  2604  abbib  2806  cleqh  2866  cleqf  2928  cbvralfw  3278  cbvralf  3323  ralab2  3644  cbvralcsf  3880  dfssf  3913  reusv2lem4  5336  cbviotaw  6453  cbviota  6455  sb8iota  6457  dffun6f  6505  findcard2  9090  aceq1  10028  bnj1385  34980  regsfromsetind  36727  bj-axseprep  37379  sbcalf  38426  alrimii  38431  aomclem6  43490  rababg  44004