Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexbidv2 Structured version   Unicode version

Theorem rexbidv2 2730
 Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 22-May-1999.)
Hypothesis
Ref Expression
rexbidv2.1
Assertion
Ref Expression
rexbidv2
Distinct variable group:   ,
Allowed substitution hints:   ()   ()   ()   ()

Proof of Theorem rexbidv2
StepHypRef Expression
1 rexbidv2.1 . . 3
21exbidv 1637 . 2
3 df-rex 2713 . 2
4 df-rex 2713 . 2
52, 3, 43bitr4g 281 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wa 360  wex 1551   wcel 1726  wrex 2708 This theorem is referenced by:  rexss  3412  rexsupp  5857  isoini  6060  exopxfr2  6413  omabs  6892  elfi2  7421  wemapso2lem  7521  ltexpi  8781  rexuz  10529  lpigen  16329  llyi  17539  nllyi  17540  elpi1  19072  xrecex  24168  mrefg2  26763  islssfg2  27148  bnj18eq1  29300  ldual1dim  29966  pmapjat1  30652 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627 This theorem depends on definitions:  df-bi 179  df-ex 1552  df-rex 2713
 Copyright terms: Public domain W3C validator