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

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