Theorem cbvalv1 2376

Description: Rule used to change bound variables, using implicit substitution. Version of cbval 2433 with a disjoint variable condition, which does not require ax-13 2407. See cbvalvw 2069 for a version with two more disjoint variable conditions, requiring fewer axioms, and cbvalv 2435 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 2370	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
6	3	biimprd 251	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜓 → 𝜑))
7	6	equcoms 2053	. . 3 ⊢ (𝑦 = 𝑥 → (𝜓 → 𝜑))
8	2, 1, 7	cbv3v 2370	. 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 1943  ax-6 2000  ax-7 2041  ax-11 2195  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  2377  cbval2v  2378  sbbib  2396  cbvsbvf  2398  sb8eulem  2629  cbvmow  2634  abbib  2835  cleqh  2895  cleqf  2956  cbvralfw  3308  cbvralf  3352  ralab2  3663  cbvralcsf  3898  dfssf  3931  reusv2lem4  5377  cbviotaw  6506  cbviota  6508  sb8iota  6510  dffun6f  6558  findcard2  9159  aceq1  10120  bnj1385  35252  regsfromsetind  37091  bj-axseprep  37752  sbcalf  38804  alrimii  38809  aomclem6  43827  rababg  44341