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

Theorem 2rexbidva 3210
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 468 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32rexbidva 3172 . 2 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝜓 ↔ ∃𝑦𝐵 𝜒))
43rexbidva 3172 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wcel 2106  wrex 3072
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 1913
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3073
This theorem is referenced by:  2reu4lem  4482  wrdl3s3  14848  bezoutlem2  16418  bezoutlem4  16420  vdwmc2  16848  lsmcom2  19433  lsmass  19447  lsmcomx  19630  lsmspsn  20541  hausdiag  22992  imasf1oxms  23841  istrkg2ld  27300  iscgra  27649  axeuclid  27810  elwwlks2  28809  elwspths2spth  28810  fusgr2wsp2nb  29176  shscom  30159  lsmssass  32078  sategoelfvb  33904  mulsval  34397  3dim0  37909  islpln5  37987  islvol5  38031  isline2  38226  isline3  38228  paddcom  38265  cdlemg2cex  39043  prprspr2  45680  pgrpgt2nabl  46412  elbigolo1  46613
  Copyright terms: Public domain W3C validator