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

Theorem 2rexbidva 3038
 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 678 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝜓𝜒))
32rexbidva 3031 . 2 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝜓 ↔ ∃𝑦𝐵 𝜒))
43rexbidva 3031 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∈ wcel 1977  ∃wrex 2897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-rex 2902 This theorem is referenced by:  wrdl3s3  13553  bezoutlem2  15095  bezoutlem4  15097  vdwmc2  15521  lsmcom2  17893  lsmass  17906  lsmcomx  18082  lsmspsn  18905  hausdiag  21258  imasf1oxms  22104  istrkg2ld  25159  iscgra  25501  axeuclid  25643  el2wlksot  26407  el2pthsot  26408  usg2spot2nb  26592  shscom  27562  3dim0  33761  islpln5  33839  islvol5  33883  isline2  34078  isline3  34080  paddcom  34117  cdlemg2cex  34897  2reu4a  39838  wwlksnwwlksnon  41121  wspthsnwspthsnon  41122  elwwlks2  41170  elwspths2spth  41171  fusgr2wsp2nb  41498  pgrpgt2nabl  41941  elbigolo1  42149
 Copyright terms: Public domain W3C validator