Theorem cbval 2269

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 2263	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
6	3	biimprd 238	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜓 → 𝜑))
7	6	equcoms 1945	. . 3 ⊢ (𝑦 = 𝑥 → (𝜓 → 𝜑))
8	2, 1, 7	cbv3 2263	. 2 ⊢ (∀𝑦𝜓 → ∀𝑥𝜑)
9	5, 8	impbii 199	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1479  Ⅎwnf 1706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-nf 1708

This theorem is referenced by:  cbvex  2270  cbvalvOLD  2272  cbval2  2277  sb8  2422  sb8eu  2501  cbvralf  3160  ralab2  3365  cbvralcsf  3558  dfss2f  3586  elintab  4478  reusv2lem4  4863  cbviota  5844  sb8iota  5846  dffun6f  5890  findcard2  8185  aceq1  8925  bnj1385  30877  sbcalf  33888  alrimii  33895  aomclem6  37448  rababg  37698