Theorem cbvalv1 2329

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1531  Ⅎwnf 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-11 2146  ax-12 2163

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-nf 1778

This theorem is referenced by:  cbvexv1  2330  cbval2v  2331  sb8fOLD  2342  sbbib  2349  cbvsbvf  2352  sb8eulem  2584  cbvmow  2589  abbib  2796  cleqh  2855  cleqf  2926  cbvralfw  3293  cbvralfwOLD  3312  cbvralf  3348  ralab2  3685  cbvralcsf  3930  dfss2f  3964  ab0OLD  4367  elintabOLD  4953  reusv2lem4  5389  cbviotaw  6492  cbviota  6495  sb8iota  6497  dffun6f  6551  findcard2  9159  findcard2OLD  9279  aceq1  10107  bnj1385  34298  sbcalf  37438  alrimii  37443  aomclem6  42256  rababg  42780