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 469 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32rexbidva 3177 . 2 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝜓 ↔ ∃𝑦𝐵 𝜒))
43rexbidva 3177 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wcel 2107  wrex 3071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072
This theorem is referenced by:  2reu4lem  4526  wrdl3s3  14913  bezoutlem2  16482  bezoutlem4  16484  vdwmc2  16912  lsmcom2  19523  lsmass  19537  lsmcomx  19724  lsmspsn  20695  hausdiag  23149  imasf1oxms  23998  mulsval  27565  mulscom  27595  addsdi  27610  mulsasslem3  27620  istrkg2ld  27711  iscgra  28060  axeuclid  28221  elwwlks2  29220  elwspths2spth  29221  fusgr2wsp2nb  29587  shscom  30572  lsmssass  32512  sategoelfvb  34410  3dim0  38328  islpln5  38406  islvol5  38450  isline2  38645  isline3  38647  paddcom  38684  cdlemg2cex  39462  prprspr2  46186  pgrpgt2nabl  47042  elbigolo1  47243
  Copyright terms: Public domain W3C validator