Theorem cbvalv1 2367

Description: Version of cbval 2423 with a disjoint variable condition, which does not require ax-13 2389. See cbvalvw 2143 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvalv 2425 for another variant. (Contributed 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 221	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
5	1, 2, 4	cbv3v 2365	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
6	3	biimprd 240	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜓 → 𝜑))
7	6	equcoms 2124	. . 3 ⊢ (𝑦 = 𝑥 → (𝜓 → 𝜑))
8	2, 1, 7	cbv3v 2365	. 2 ⊢ (∀𝑦𝜓 → ∀𝑥𝜑)
9	5, 8	impbii 201	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

Syntax hints:   → wi 4   ↔ wb 198  ∀wal 1654  Ⅎwnf 1882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-10 2192  ax-11 2207  ax-12 2220

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-nf 1883

This theorem is referenced by:  cbvexv1  2368  sb8v  2376  sb8eulem  2686  cleqh  2929  cbvralf  3377  ralab2  3594  cbvralcsf  3789  dfss2f  3818  elintab  4710  reusv2lem4  5103  cbviota  6095  sb8iota  6097  dffun6f  6141  findcard2  8475  aceq1  9260  bnj1385  31445  bj-cbvalvv  33265  bj-cbval2v  33269  bj-abbi  33299  sbcalf  34457  alrimii  34463  aomclem6  38471  rababg  38719