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

Theorem cbval 2416
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 2410 . 2 (∀𝑥𝜑 → ∀𝑦𝜓)
63biimprd 238 . . . 4 (𝑥 = 𝑦 → (𝜓𝜑))
76equcoms 2102 . . 3 (𝑦 = 𝑥 → (𝜓𝜑))
82, 1, 7cbv3 2410 . 2 (∀𝑦𝜓 → ∀𝑥𝜑)
95, 8impbii 199 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1630  wnf 1857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-nf 1859
This theorem is referenced by:  cbvex  2417  cbvalvOLD  2419  cbval2  2424  sb8  2561  sb8eu  2641  cbvralf  3304  ralab2  3512  cbvralcsf  3706  dfss2f  3735  elintab  4639  reusv2lem4  5021  cbviota  6017  sb8iota  6019  dffun6f  6063  findcard2  8367  aceq1  9150  bnj1385  31231  sbcalf  34248  alrimii  34255  aomclem6  38149  rababg  38399
  Copyright terms: Public domain W3C validator