Theorem cbvalv1 2357

Description: Rule used to change bound variables, using implicit substitution. Version of cbval 2412 with a disjoint variable condition, which does not require ax-13 2386. See cbvalvw 2039 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvalv 2414 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 231	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
5	1, 2, 4	cbv3v 2351	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
6	3	biimprd 250	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜓 → 𝜑))
7	6	equcoms 2023	. . 3 ⊢ (𝑦 = 𝑥 → (𝜓 → 𝜑))
8	2, 1, 7	cbv3v 2351	. 2 ⊢ (∀𝑦𝜓 → ∀𝑥𝜑)
9	5, 8	impbii 211	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1531  Ⅎwnf 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-11 2157  ax-12 2173

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-nf 1781

This theorem is referenced by:  cbvexv1  2358  cbval2v  2359  cbval2vOLD  2360  sb8v  2369  sbbib  2376  sb8eulem  2680  abbi  2888  cleqh  2936  cleqf  3010  cbvralfw  3437  cbvralf  3439  ralab2  3687  ralab2OLD  3688  cbvralcsf  3924  dfss2f  3957  elintab  4879  reusv2lem4  5293  cbviotaw  6315  cbviota  6317  sb8iota  6319  dffun6f  6363  findcard2  8752  aceq1  9537  bnj1385  32099  sbcalf  35386  alrimii  35391  aomclem6  39652  rababg  39926