Theorem cbval 2307

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 13-May-1993.) (Revised by Mario Carneiro, 3-Oct-2016.)

Hypotheses

Ref	Expression
cbval.1	⊢ Ⅎ𝑦𝜑
cbval.2	⊢ Ⅎ𝑥𝜓
cbval.3	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbval	⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

Proof of Theorem cbval

Step	Hyp	Ref	Expression
1		cbval.1	. . 3 ⊢ Ⅎ𝑦𝜑
2		cbval.2	. . 3 ⊢ Ⅎ𝑥𝜓
3		cbval.3	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	3	biimpd 219	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
5	1, 2, 4	cbv3 2301	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
6	3	biimprd 238	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜓 → 𝜑))
7	6	equcoms 1993	. . 3 ⊢ (𝑦 = 𝑥 → (𝜓 → 𝜑))
8	2, 1, 7	cbv3 2301	. 2 ⊢ (∀𝑦𝜓 → ∀𝑥𝜑)
9	5, 8	impbii 199	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1521  Ⅎwnf 1748

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-nf 1750

This theorem is referenced by:  cbvex  2308  cbvalvOLD  2310  cbval2  2315  sb8  2452  sb8eu  2532  cbvralf  3195  ralab2  3404  cbvralcsf  3598  dfss2f  3627  elintab  4519  reusv2lem4  4902  cbviota  5894  sb8iota  5896  dffun6f  5940  findcard2  8241  aceq1  8978  bnj1385  31029  sbcalf  34047  alrimii  34054  aomclem6  37946  rababg  38196