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

Theorem cbvexv 2418
 Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-10 2166. (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 307 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
32cbvalv 2416 . . 3 (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
43notbii 309 . 2 (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
5 df-ex 1852 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
6 df-ex 1852 . 2 (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
74, 5, 63bitr4i 292 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196  ∀wal 1628  ∃wex 1851 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-11 2181  ax-12 2194  ax-13 2389 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1852 This theorem is referenced by:  cbvex2v  2430  eujust  2607  euind  3532  reuind  3550  cbvopab2v  4877  bm1.3ii  4934  reusv2lem2  5016  reusv2lem2OLD  5017  relop  5426  dmcoss  5538  fv3  6365  exfo  6538  zfun  7113  wfrlem1  7581  ac6sfi  8367  brwdom2  8641  aceq1  9128  aceq0  9129  aceq3lem  9131  dfac4  9133  kmlem2  9163  kmlem13  9174  axdc4lem  9467  zfac  9472  zfcndun  9627  zfcndac  9631  sup2  11169  supmul  11185  climmo  14485  summo  14645  prodmo  14863  gsumval3eu  18503  elpt  21575  bnj1185  31169  frrlem1  32084  fdc  33852  axc11next  39107  fnchoice  39685
 Copyright terms: Public domain W3C validator