Theorem cbvalv1 2339

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784

This theorem is referenced by:  cbvexv1  2340  cbval2v  2341  sb8fOLD  2353  sbbib  2360  cbvsbvf  2362  sb8eulem  2592  cbvmow  2597  abbib  2799  cleqh  2858  cleqf  2921  cbvralfw  3280  cbvralf  3336  ralab2  3671  cbvralcsf  3907  dfssf  3940  elintabOLD  4926  reusv2lem4  5359  cbviotaw  6474  cbviota  6476  sb8iota  6478  dffun6f  6532  findcard2  9134  aceq1  10077  bnj1385  34829  sbcalf  38115  alrimii  38120  aomclem6  43055  rababg  43570