Theorem cbvalv1 2373

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1568  Ⅎwnf 1813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-11 2192  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-nf 1814

This theorem is referenced by:  cbvexv1  2374  cbval2v  2375  sbbib  2393  cbvsbvf  2395  sb8eulem  2626  cbvmow  2631  abbib  2832  cleqh  2892  cleqf  2953  cbvralfw  3305  cbvralf  3349  ralab2  3661  cbvralcsf  3896  dfssf  3929  reusv2lem4  5374  cbviotaw  6501  cbviota  6503  sb8iota  6505  dffun6f  6553  findcard2  9150  aceq1  10102  bnj1385  35201  regsfromsetind  37031  bj-axseprep  37692  sbcalf  38744  alrimii  38749  aomclem6  43769  rababg  44283