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

Theorem 2rexbidva 3218
Description: Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 15-Dec-2004.)
Hypothesis
Ref Expression
2ralbidva.1 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝜓𝜒))
Assertion
Ref Expression
2rexbidva (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Distinct variable groups:   𝑥,𝑦,𝜑   𝑦,𝐴
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem 2rexbidva
StepHypRef Expression
1 2ralbidva.1 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝜓𝜒))
21anassrs 467 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32rexbidva 3175 . 2 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝜓 ↔ ∃𝑦𝐵 𝜒))
43rexbidva 3175 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wcel 2106  wrex 3068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-rex 3069
This theorem is referenced by:  2reu4lem  4528  wrdl3s3  14998  bezoutlem2  16574  bezoutlem4  16576  vdwmc2  17013  lsmcom2  19688  lsmass  19702  lsmcomx  19889  lsmspsn  21101  hausdiag  23669  imasf1oxms  24518  mulsval  28150  mulscom  28180  addsdi  28196  mulsasslem3  28206  mulsunif2lem  28210  istrkg2ld  28483  iscgra  28832  axeuclid  28993  elwwlks2  29996  elwspths2spth  29997  fusgr2wsp2nb  30363  shscom  31348  lsmssass  33410  sategoelfvb  35404  3dim0  39440  islpln5  39518  islvol5  39562  isline2  39757  isline3  39759  paddcom  39796  cdlemg2cex  40574  prprspr2  47443  pgrpgt2nabl  48211  elbigolo1  48407
  Copyright terms: Public domain W3C validator