MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbval Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 cbval.1 . . 3 𝑦𝜑
2 cbval.2 . . 3 𝑥𝜓
3 cbval.3 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
43biimpd 219 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
51, 2, 4cbv3 2263 . 2 (∀𝑥𝜑 → ∀𝑦𝜓)
63biimprd 238 . . . 4 (𝑥 = 𝑦 → (𝜓𝜑))
76equcoms 1945 . . 3 (𝑦 = 𝑥 → (𝜓𝜑))
82, 1, 7cbv3 2263 . 2 (∀𝑦𝜓 → ∀𝑥𝜑)
95, 8impbii 199 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator