Theorem cbvalv1 2341

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1534  Ⅎwnf 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-11 2154  ax-12 2174

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

This theorem is referenced by:  cbvexv1  2342  cbval2v  2343  sb8fOLD  2354  sbbib  2361  cbvsbvf  2363  sb8eulem  2595  cbvmow  2600  abbib  2808  cleqh  2868  cleqf  2931  cbvralfw  3301  cbvralf  3357  ralab2  3705  cbvralcsf  3952  dfssf  3985  elintabOLD  4963  reusv2lem4  5406  cbviotaw  6522  cbviota  6524  sb8iota  6526  dffun6f  6580  findcard2  9202  aceq1  10154  bnj1385  34824  sbcalf  38100  alrimii  38105  aomclem6  43047  rababg  43563