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

Theorem cbvalv1 2363
 Description: Rule used to change bound variables, using implicit substitution. Version of cbval 2418 with a disjoint variable condition, which does not require ax-13 2392. See cbvalvw 2044 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvalv 2420 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 232 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
51, 2, 4cbv3v 2357 . 2 (∀𝑥𝜑 → ∀𝑦𝜓)
63biimprd 251 . . . 4 (𝑥 = 𝑦 → (𝜓𝜑))
76equcoms 2028 . . 3 (𝑦 = 𝑥 → (𝜓𝜑))
82, 1, 7cbv3v 2357 . 2 (∀𝑦𝜓 → ∀𝑥𝜑)
95, 8impbii 212 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536  Ⅎwnf 1785 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-11 2162  ax-12 2179 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786 This theorem is referenced by:  cbvexv1  2364  cbval2v  2365  cbval2vOLD  2366  sb8v  2375  sbbib  2382  sb8eulem  2685  cbvmow  2689  abbi  2891  cbvabw  2893  cleqh  2939  cleqf  3010  cbvralfw  3421  cbvralfwOLD  3422  cbvralf  3424  ralab2  3674  ralab2OLD  3675  cbvralcsf  3908  dfss2f  3943  elintab  4873  reusv2lem4  5289  cbviotaw  6309  cbviota  6311  sb8iota  6313  dffun6f  6357  findcard2  8749  aceq1  9535  bnj1385  32129  sbcalf  35462  alrimii  35467  aomclem6  39856  rababg  40126
 Copyright terms: Public domain W3C validator