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

Theorem ceqsrexv 3324
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 2918 . . 3 (∃𝑥𝐵 (𝑥 = 𝐴𝜑) ↔ ∃𝑥(𝑥𝐵 ∧ (𝑥 = 𝐴𝜑)))
2 an12 837 . . . 4 ((𝑥 = 𝐴 ∧ (𝑥𝐵𝜑)) ↔ (𝑥𝐵 ∧ (𝑥 = 𝐴𝜑)))
32exbii 1772 . . 3 (∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝐵𝜑)) ↔ ∃𝑥(𝑥𝐵 ∧ (𝑥 = 𝐴𝜑)))
41, 3bitr4i 267 . 2 (∃𝑥𝐵 (𝑥 = 𝐴𝜑) ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝐵𝜑)))
5 eleq1 2692 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
6 ceqsrexv.1 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
75, 6anbi12d 746 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
87ceqsexgv 3323 . . 3 (𝐴𝐵 → (∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝐵𝜑)) ↔ (𝐴𝐵𝜓)))
98bianabs 923 . 2 (𝐴𝐵 → (∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝐵𝜑)) ↔ 𝜓))
104, 9syl5bb 272 1 (𝐴𝐵 → (∃𝑥𝐵 (𝑥 = 𝐴𝜑) ↔ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wex 1701  wcel 1992  wrex 2913
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 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-12 2049  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-rex 2918  df-v 3193
This theorem is referenced by:  ceqsrexbv  3325  ceqsrex2v  3326  reuxfr2d  4856  f1oiso  6556  creur  10959  creui  10960  deg1ldg  23751  ulm2  24038  iscgra1  25597  reuxfr3d  29169  poimirlem24  33032  eqlkr3  33835  diclspsn  35930  rmxdiophlem  37029  expdiophlem1  37035  expdiophlem2  37036
  Copyright terms: Public domain W3C validator