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

Theorem 2rexbidva 3264
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 468 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32rexbidva 3261 . 2 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝜓 ↔ ∃𝑦𝐵 𝜒))
43rexbidva 3261 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wcel 2083  wrex 3108
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-rex 3113
This theorem is referenced by:  2reu4lem  4385  wrdl3s3  14164  bezoutlem2  15721  bezoutlem4  15723  vdwmc2  16148  lsmcom2  18514  lsmass  18527  lsmcomx  18703  lsmspsn  19550  hausdiag  21941  imasf1oxms  22786  istrkg2ld  25932  iscgra  26281  axeuclid  26436  elwwlks2  27431  elwspths2spth  27432  fusgr2wsp2nb  27801  shscom  28783  sategoelfvb  32276  3dim0  36145  islpln5  36223  islvol5  36267  isline2  36462  isline3  36464  paddcom  36501  cdlemg2cex  37279  prprspr2  43184  pgrpgt2nabl  43916  elbigolo1  44120
  Copyright terms: Public domain W3C validator