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

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

Proof of Theorem 2rexbidva
StepHypRef Expression
1 2rexbidva.1 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝜓𝜒))
21anassrs 471 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32rexbidva 3220 . 2 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝜓 ↔ ∃𝑦𝐵 𝜒))
43rexbidva 3220 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∈ wcel 2111  ∃wrex 3071 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 1911 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-rex 3076 This theorem is referenced by:  2reu4lem  4418  wrdl3s3  14373  bezoutlem2  15939  bezoutlem4  15941  vdwmc2  16370  lsmcom2  18847  lsmass  18862  lsmcomx  19044  lsmspsn  19924  hausdiag  22345  imasf1oxms  23191  istrkg2ld  26353  iscgra  26702  axeuclid  26856  elwwlks2  27851  elwspths2spth  27852  fusgr2wsp2nb  28218  shscom  29201  lsmssass  31111  sategoelfvb  32897  3dim0  37033  islpln5  37111  islvol5  37155  isline2  37350  isline3  37352  paddcom  37389  cdlemg2cex  38167  prprspr2  44403  pgrpgt2nabl  45135  elbigolo1  45336
 Copyright terms: Public domain W3C validator