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

Theorem cbvalv1 2343
Description: Rule used to change bound variables, using implicit substitution. Version of cbval 2403 with a disjoint variable condition, which does not require ax-13 2377. See cbvalvw 2035 for a version with two more disjoint variable conditions, requiring fewer axioms, and cbvalv 2405 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 229 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
51, 2, 4cbv3v 2337 . 2 (∀𝑥𝜑 → ∀𝑦𝜓)
63biimprd 248 . . . 4 (𝑥 = 𝑦 → (𝜓𝜑))
76equcoms 2019 . . 3 (𝑦 = 𝑥 → (𝜓𝜑))
82, 1, 7cbv3v 2337 . 2 (∀𝑦𝜓 → ∀𝑥𝜑)
95, 8impbii 209 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1538  wnf 1783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-11 2157  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784
This theorem is referenced by:  cbvexv1  2344  cbval2v  2345  sb8fOLD  2357  sbbib  2364  cbvsbvf  2366  sb8eulem  2598  cbvmow  2603  abbib  2811  cleqh  2871  cleqf  2934  cbvralfw  3304  cbvralf  3360  ralab2  3703  cbvralcsf  3941  dfssf  3974  elintabOLD  4959  reusv2lem4  5401  cbviotaw  6521  cbviota  6523  sb8iota  6525  dffun6f  6579  findcard2  9204  aceq1  10157  bnj1385  34846  sbcalf  38121  alrimii  38126  aomclem6  43071  rababg  43587
  Copyright terms: Public domain W3C validator