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

Theorem cbvalv1 2367
Description: Version of cbval 2423 with a disjoint variable condition, which does not require ax-13 2389. See cbvalvw 2143 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvalv 2425 for another variant. (Contributed 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 221 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
51, 2, 4cbv3v 2365 . 2 (∀𝑥𝜑 → ∀𝑦𝜓)
63biimprd 240 . . . 4 (𝑥 = 𝑦 → (𝜓𝜑))
76equcoms 2124 . . 3 (𝑦 = 𝑥 → (𝜓𝜑))
82, 1, 7cbv3v 2365 . 2 (∀𝑦𝜓 → ∀𝑥𝜑)
95, 8impbii 201 1 (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wal 1654  wnf 1882
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-10 2192  ax-11 2207  ax-12 2220
This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-nf 1883
This theorem is referenced by:  cbvexv1  2368  sb8v  2376  sb8eulem  2686  cleqh  2929  cbvralf  3377  ralab2  3594  cbvralcsf  3789  dfss2f  3818  elintab  4710  reusv2lem4  5103  cbviota  6095  sb8iota  6097  dffun6f  6141  findcard2  8475  aceq1  9260  bnj1385  31445  bj-cbvalvv  33265  bj-cbval2v  33269  bj-abbi  33299  sbcalf  34457  alrimii  34463  aomclem6  38471  rababg  38719
  Copyright terms: Public domain W3C validator