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

Theorem cbvalv1 2331
Description: Rule used to change bound variables, using implicit substitution. Version of cbval 2391 with a disjoint variable condition, which does not require ax-13 2365. See cbvalvw 2031 for a version with two more disjoint variable conditions, requiring fewer axioms, and cbvalv 2393 for another variant. (Contributed by NM, 13-May-1993.) (Revised by BJ, 31-May-2019.)
Hypotheses
Ref Expression
cbvalv1.nf1 𝑦𝜑
cbvalv1.nf2 𝑥𝜓
cbvalv1.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvalv1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem cbvalv1
StepHypRef Expression
1 cbvalv1.nf1 . . 3 𝑦𝜑
2 cbvalv1.nf2 . . 3 𝑥𝜓
3 cbvalv1.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
43biimpd 228 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
51, 2, 4cbv3v 2325 . 2 (∀𝑥𝜑 → ∀𝑦𝜓)
63biimprd 247 . . . 4 (𝑥 = 𝑦 → (𝜓𝜑))
76equcoms 2015 . . 3 (𝑦 = 𝑥 → (𝜓𝜑))
82, 1, 7cbv3v 2325 . 2 (∀𝑦𝜓 → ∀𝑥𝜑)
95, 8impbii 208 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1531  wnf 1777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-11 2146  ax-12 2166
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-nf 1778
This theorem is referenced by:  cbvexv1  2332  cbval2v  2333  sb8fOLD  2344  sbbib  2351  cbvsbvf  2354  sb8eulem  2586  cbvmow  2591  abbib  2797  cleqh  2855  cleqf  2923  cbvralfw  3291  cbvralf  3343  ralab2  3689  cbvralcsf  3934  dfssf  3967  ab0OLD  4377  elintabOLD  4963  reusv2lem4  5401  cbviotaw  6508  cbviota  6511  sb8iota  6513  dffun6f  6567  findcard2  9189  findcard2OLD  9309  aceq1  10142  bnj1385  34594  sbcalf  37718  alrimii  37723  aomclem6  42625  rababg  43146
  Copyright terms: Public domain W3C validator