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

Theorem ceqsrexv 3655
Description: Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 30-Apr-2004.)
Hypothesis
Ref Expression
ceqsrexv.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
ceqsrexv (𝐴𝐵 → (∃𝑥𝐵 (𝑥 = 𝐴𝜑) ↔ 𝜓))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ceqsrexv
StepHypRef Expression
1 df-rex 3071 . . 3 (∃𝑥𝐵 (𝑥 = 𝐴𝜑) ↔ ∃𝑥(𝑥𝐵 ∧ (𝑥 = 𝐴𝜑)))
2 an12 645 . . . 4 ((𝑥 = 𝐴 ∧ (𝑥𝐵𝜑)) ↔ (𝑥𝐵 ∧ (𝑥 = 𝐴𝜑)))
32exbii 1848 . . 3 (∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝐵𝜑)) ↔ ∃𝑥(𝑥𝐵 ∧ (𝑥 = 𝐴𝜑)))
41, 3bitr4i 278 . 2 (∃𝑥𝐵 (𝑥 = 𝐴𝜑) ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝐵𝜑)))
5 eleq1 2829 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
6 ceqsrexv.1 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
75, 6anbi12d 632 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
87ceqsexgv 3654 . . 3 (𝐴𝐵 → (∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝐵𝜑)) ↔ (𝐴𝐵𝜓)))
98bianabs 541 . 2 (𝐴𝐵 → (∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝐵𝜑)) ↔ 𝜓))
104, 9bitrid 283 1 (𝐴𝐵 → (∃𝑥𝐵 (𝑥 = 𝐴𝜑) ↔ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wex 1779  wcel 2108  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071
This theorem is referenced by:  ceqsrexbv  3656  ceqsrex2v  3658  reuxfrd  3754  f1oiso  7371  creur  12260  creui  12261  deg1ldg  26131  ulm2  26428  iscgra1  28818  reuxfrdf  32510  poimirlem24  37651  eqlkr3  39102  diclspsn  41196  rmxdiophlem  43027  expdiophlem1  43033  expdiophlem2  43034
  Copyright terms: Public domain W3C validator