Theorem cbvalv1 2371

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-11 2194  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817

This theorem is used by:  cbvexv1  2372  cbval2v  2373  sbbib  2391  cbvsbvf  2393  sb8eulem  2624  cbvmow  2629  abbib  2830  cleqh  2890  cleqf  2951  cbvralfw  3303  cbvralf  3346  ralab2  3655  cbvralcsf  3889  dfssf  3922  reusv2lem4  5363  cbviotaw  6494  cbviota  6496  sb8iota  6498  dffun6f  6546  findcard2  9164  aceq1  10177  bnj1385  35445  regsfromsetind  37297  bj-axseprep  37958  sbcalf  39014  alrimii  39019  aomclem6  44019  rababg  44533