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

Theorem cbvexv 2274
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-10 2016. (Revised by Wolf Lammen, 17-Jul-2021.)
Hypothesis
Ref Expression
cbvalv.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvexv (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Distinct variable groups:   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvexv
StepHypRef Expression
1 cbvalv.1 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
21notbid 308 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
32cbvalv 2272 . . 3 (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
43notbii 310 . 2 (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
5 df-ex 1702 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
6 df-ex 1702 . 2 (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
74, 5, 63bitr4i 292 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wal 1478  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-nf 1707
This theorem is referenced by:  cbvex2v  2286  eujust  2471  euind  3375  reuind  3393  cbvopab2v  4689  bm1.3ii  4744  reusv2lem2  4829  reusv2lem2OLD  4830  relop  5232  dmcoss  5345  fv3  6163  exfo  6333  zfun  6903  wfrlem1  7359  ac6sfi  8148  brwdom2  8422  aceq1  8884  aceq0  8885  aceq3lem  8887  dfac4  8889  kmlem2  8917  kmlem13  8928  axdc4lem  9221  zfac  9226  zfcndun  9381  zfcndac  9385  sup2  10923  supmul  10939  climmo  14222  summo  14381  prodmo  14591  gsumval3eu  18226  elpt  21285  bnj1185  30569  frrlem1  31478  fdc  33170  axc11next  38086  fnchoice  38668
  Copyright terms: Public domain W3C validator