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

Theorem 2rexbidva 3208
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 3167 . 2 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝜓 ↔ ∃𝑦𝐵 𝜒))
43rexbidva 3167 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wcel 2099  wrex 3060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-rex 3061
This theorem is referenced by:  2reu4lem  4521  wrdl3s3  14964  bezoutlem2  16534  bezoutlem4  16536  vdwmc2  16974  lsmcom2  19647  lsmass  19661  lsmcomx  19848  lsmspsn  21056  hausdiag  23635  imasf1oxms  24484  mulsval  28105  mulscom  28135  addsdi  28151  mulsasslem3  28161  mulsunif2lem  28165  istrkg2ld  28382  iscgra  28731  axeuclid  28892  elwwlks2  29895  elwspths2spth  29896  fusgr2wsp2nb  30262  shscom  31247  lsmssass  33281  sategoelfvb  35258  3dim0  39167  islpln5  39245  islvol5  39289  isline2  39484  isline3  39486  paddcom  39523  cdlemg2cex  40301  prprspr2  47124  pgrpgt2nabl  47779  elbigolo1  47979
  Copyright terms: Public domain W3C validator