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

Theorem 2rexbidva 3050
Description: Formula-building rule for restricted existential quantifiers (deduction rule). (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 679 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32rexbidva 3043 . 2 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝜓 ↔ ∃𝑦𝐵 𝜒))
43rexbidva 3043 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  wcel 1987  wrex 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-rex 2913
This theorem is referenced by:  wrdl3s3  13646  bezoutlem2  15188  bezoutlem4  15190  vdwmc2  15614  lsmcom2  17998  lsmass  18011  lsmcomx  18187  lsmspsn  19012  hausdiag  21367  imasf1oxms  22213  istrkg2ld  25272  iscgra  25614  axeuclid  25756  wwlksnwwlksnon  26692  wspthsnwspthsnon  26693  elwwlks2  26741  elwspths2spth  26742  fusgr2wsp2nb  27069  shscom  28045  3dim0  34250  islpln5  34328  islvol5  34372  isline2  34567  isline3  34569  paddcom  34606  cdlemg2cex  35386  2reu4a  40514  pgrpgt2nabl  41456  elbigolo1  41664
  Copyright terms: Public domain W3C validator