Theorem cbvalv1 2374

Description: Rule used to change bound variables, using implicit substitution. Version of cbval 2430 with a disjoint variable condition, which does not require ax-13 2404. See cbvalvw 2071 for a version with two more disjoint variable conditions, requiring fewer axioms, and cbvalv 2432 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 2368	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
6	3	biimprd 251	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜓 → 𝜑))
7	6	equcoms 2055	. . 3 ⊢ (𝑦 = 𝑥 → (𝜓 → 𝜑))
8	2, 1, 7	cbv3v 2368	. 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 1945  ax-6 2002  ax-7 2043  ax-11 2197  ax-12 2216

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

This theorem is used by:  cbvexv1  2375  cbval2v  2376  sbbib  2393  cbvsbvf  2395  sb8eulem  2626  cbvmow  2631  abbibOLD  2833  cleqh  2893  cleqf  2954  cbvralfw  3306  cbvralf  3349  ralab2  3658  cbvralcsf  3893  dfssf  3904  reusv2lem4  5368  cbviotaw  6522  cbviota  6524  sb8iota  6526  dffun6f  6576  findcard2  9211  aceq1  10226  bnj1385  35545  regsfromsetind  37518  bj-axseprep  38194  sbcalf  39249  alrimii  39254  aomclem6  44265  rababg  44778