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

Theorem 2rexbidva 3215
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 466 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32rexbidva 3174 . 2 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝜓 ↔ ∃𝑦𝐵 𝜒))
43rexbidva 3174 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wcel 2104  wrex 3068
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 1911
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-rex 3069
This theorem is referenced by:  2reu4lem  4524  wrdl3s3  14917  bezoutlem2  16486  bezoutlem4  16488  vdwmc2  16916  lsmcom2  19564  lsmass  19578  lsmcomx  19765  lsmspsn  20839  hausdiag  23369  imasf1oxms  24218  mulsval  27804  mulscom  27834  addsdi  27849  mulsasslem3  27859  istrkg2ld  27978  iscgra  28327  axeuclid  28488  elwwlks2  29487  elwspths2spth  29488  fusgr2wsp2nb  29854  shscom  30839  lsmssass  32786  sategoelfvb  34708  3dim0  38631  islpln5  38709  islvol5  38753  isline2  38948  isline3  38950  paddcom  38987  cdlemg2cex  39765  prprspr2  46484  pgrpgt2nabl  47130  elbigolo1  47330
  Copyright terms: Public domain W3C validator