Theorem cbvalv1 2375

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1561  Ⅎwnf 1806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-11 2194  ax-12 2215

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-nf 1807

This theorem is referenced by:  cbvexv1  2376  cbval2v  2377  sbbib  2395  cbvsbvf  2397  sb8eulem  2628  cbvmow  2633  abbib  2834  cleqh  2894  cleqf  2955  cbvralfw  3305  cbvralf  3350  ralab2  3663  cbvralcsf  3897  dfssf  3930  reusv2lem4  5362  cbviotaw  6488  cbviota  6490  sb8iota  6492  dffun6f  6540  findcard2  9137  aceq1  10089  bnj1385  35132  regsfromsetind  36907  bj-axseprep  37566  sbcalf  38620  alrimii  38625  aomclem6  43643  rababg  44157