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