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

Theorem rexlimddvcbvw 40835
 Description: Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 40834. The equivalent of this theorem without the bound variable change is rexlimddv 3283. Version of rexlimddvcbv 40836 with a disjoint variable condition, which does not require ax-13 2392. (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 3435 . . 3 (∃𝑥𝐴 𝜃 ↔ ∃𝑦𝐴 𝜒)
4 rexlimddvcbvw.2 . . . 4 ((𝜑 ∧ (𝑦𝐴𝜒)) → 𝜓)
54rexlimdvaa 3277 . . 3 (𝜑 → (∃𝑦𝐴 𝜒𝜓))
63, 5syl5bi 245 . 2 (𝜑 → (∃𝑥𝐴 𝜃𝜓))
71, 6mpd 15 1 (𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∈ wcel 2115  ∃wrex 3134 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-clel 2896  df-ral 3138  df-rex 3139 This theorem is referenced by:  mnuprdlem1  40904  mnuprdlem2  40905
 Copyright terms: Public domain W3C validator