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 2399 with a disjoint variable condition, which does not require ax-13 2373. See cbvalvw 2044 for a version with two more disjoint variable conditions, requiring fewer axioms, and cbvalv 2401 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 2337 . 2 (∀𝑥𝜑 → ∀𝑦𝜓)
63biimprd 251 . . . 4 (𝑥 = 𝑦 → (𝜓𝜑))
76equcoms 2028 . . 3 (𝑦 = 𝑥 → (𝜓𝜑))
82, 1, 7cbv3v 2337 . 2 (∀𝑦𝜓 → ∀𝑥𝜑)
95, 8impbii 212 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wal 1541  wnf 1791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-11 2160  ax-12 2177
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-nf 1792
This theorem is referenced by:  cbvexv1  2344  cbval2v  2345  cbval2vOLD  2346  sb8v  2355  sbbib  2362  sbievg  2364  sb8eulem  2599  cbvmow  2604  abbi  2812  cleqh  2863  cleqf  2938  cbvralfw  3359  cbvralfwOLD  3360  cbvralf  3362  ralab2  3627  ralab2OLD  3628  cbvralcsf  3873  dfss2f  3907  ab0OLD  4307  elintab  4887  reusv2lem4  5311  cbviotaw  6366  cbviota  6369  sb8iota  6371  dffun6f  6415  findcard2  8868  findcard2OLD  8943  aceq1  9761  bnj1385  32556  sbcalf  36046  alrimii  36051  aomclem6  40635  rababg  40905
  Copyright terms: Public domain W3C validator