Users' Mathboxes Mathbox for Rohan Ridenour < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rexlimddvcbvw Structured version   Visualization version   GIF version

Theorem rexlimddvcbvw 43697
Description: Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 43696. The equivalent of this theorem without the bound variable change is rexlimddv 3151. Version of rexlimddvcbv 43698 with a disjoint variable condition, which does not require ax-13 2365. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Revised by Gino Giotto, 2-Apr-2024.)
Hypotheses
Ref Expression
rexlimddvcbvw.1 (𝜑 → ∃𝑥𝐴 𝜃)
rexlimddvcbvw.2 ((𝜑 ∧ (𝑦𝐴𝜒)) → 𝜓)
rexlimddvcbvw.3 (𝑥 = 𝑦 → (𝜃𝜒))
Assertion
Ref Expression
rexlimddvcbvw (𝜑𝜓)
Distinct variable groups:   𝜑,𝑦   𝜓,𝑦   𝜒,𝑥   𝜃,𝑦   𝑥,𝑦,𝐴
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝜒(𝑦)   𝜃(𝑥)

Proof of Theorem rexlimddvcbvw
StepHypRef Expression
1 rexlimddvcbvw.1 . 2 (𝜑 → ∃𝑥𝐴 𝜃)
2 rexlimddvcbvw.3 . . . 4 (𝑥 = 𝑦 → (𝜃𝜒))
32cbvrexvw 3226 . . 3 (∃𝑥𝐴 𝜃 ↔ ∃𝑦𝐴 𝜒)
4 rexlimddvcbvw.2 . . . 4 ((𝜑 ∧ (𝑦𝐴𝜒)) → 𝜓)
54rexlimdvaa 3146 . . 3 (𝜑 → (∃𝑦𝐴 𝜒𝜓))
63, 5biimtrid 241 . 2 (𝜑 → (∃𝑥𝐴 𝜃𝜓))
71, 6mpd 15 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wcel 2098  wrex 3060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-clel 2802  df-rex 3061
This theorem is referenced by:  mnuprdlem1  43770  mnuprdlem2  43771
  Copyright terms: Public domain W3C validator