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

Theorem cbval 2259
 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 218 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
51, 2, 4cbv3 2253 . 2 (∀𝑥𝜑 → ∀𝑦𝜓)
63biimprd 237 . . . 4 (𝑥 = 𝑦 → (𝜓𝜑))
76equcoms 1934 . . 3 (𝑦 = 𝑥 → (𝜓𝜑))
82, 1, 7cbv3 2253 . 2 (∀𝑦𝜓 → ∀𝑥𝜑)
95, 8impbii 198 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473  Ⅎwnf 1699 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-nf 1701 This theorem is referenced by:  cbvex  2260  cbvalvOLD  2262  cbval2  2267  sb8  2412  sb8eu  2491  cbvralf  3141  ralab2  3338  cbvralcsf  3531  dfss2f  3559  elintab  4422  reusv2lem4  4798  cbviota  5773  sb8iota  5775  dffun6f  5818  findcard2  8085  aceq1  8823  bnj1385  30157  sbcalf  33087  alrimii  33094  aomclem6  36647  rababg  36898  dfcleqf  38281
 Copyright terms: Public domain W3C validator