Theorem cbvalv1 2343

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-11 2162  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785

This theorem is referenced by:  cbvexv1  2344  cbval2v  2345  sbbib  2363  cbvsbvf  2365  sb8eulem  2595  cbvmow  2600  abbib  2802  cleqh  2862  cleqf  2924  cbvralfw  3273  cbvralf  3327  ralab2  3652  cbvralcsf  3888  dfssf  3921  reusv2lem4  5341  cbviotaw  6449  cbviota  6451  sb8iota  6453  dffun6f  6501  findcard2  9081  aceq1  10015  bnj1385  34865  sbcalf  38175  alrimii  38180  aomclem6  43177  rababg  43692