Theorem cbvalv1 2345

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

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

This theorem is referenced by:  cbvexv1  2346  cbval2v  2347  sbbib  2365  cbvsbvf  2367  sb8eulem  2598  cbvmow  2603  abbib  2805  cleqh  2865  cleqf  2927  cbvralfw  3276  cbvralf  3330  ralab2  3655  cbvralcsf  3891  dfssf  3924  reusv2lem4  5346  cbviotaw  6455  cbviota  6457  sb8iota  6459  dffun6f  6507  findcard2  9089  aceq1  10027  bnj1385  34988  regsfromsetind  36669  sbcalf  38315  alrimii  38320  aomclem6  43301  rababg  43815