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

Theorem cbvalv1 2338
Description: Rule used to change bound variables, using implicit substitution. Version of cbval 2397 with a disjoint variable condition, which does not require ax-13 2371. See cbvalvw 2040 for a version with two more disjoint variable conditions, requiring fewer axioms, and cbvalv 2399 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 2332 . 2 (∀𝑥𝜑 → ∀𝑦𝜓)
63biimprd 248 . . . 4 (𝑥 = 𝑦 → (𝜓𝜑))
76equcoms 2024 . . 3 (𝑦 = 𝑥 → (𝜓𝜑))
82, 1, 7cbv3v 2332 . 2 (∀𝑦𝜓 → ∀𝑥𝜑)
95, 8impbii 208 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1540  wnf 1786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-11 2155  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-nf 1787
This theorem is referenced by:  cbvexv1  2339  cbval2v  2340  sb8fOLD  2351  sbbib  2358  sbievg  2360  sb8eulem  2597  cbvmow  2602  abbi  2809  cleqh  2868  cleqf  2939  cbvralfw  3290  cbvralfwOLD  3307  cbvralf  3336  ralab2  3660  cbvralcsf  3905  dfss2f  3939  ab0OLD  4340  elintabOLD  4925  reusv2lem4  5361  cbviotaw  6460  cbviota  6463  sb8iota  6465  dffun6f  6519  findcard2  9115  findcard2OLD  9235  aceq1  10060  bnj1385  33484  sbcalf  36602  alrimii  36607  aomclem6  41415  rababg  41920
  Copyright terms: Public domain W3C validator