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

Theorem exbid 1886
Description: Formula-building rule for existential quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
exbid.1
exbid.2
Assertion
Ref Expression
exbid

Proof of Theorem exbid
StepHypRef Expression
1 exbid.1 . . 3
21nfri 1874 . 2
3 exbid.2 . 2
42, 3exbidh 1676 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  E.wex 1612  F/wnf 1616
This theorem is referenced by:  mobid  2303  rexbida  2963  rexeqf  3051  opabbid  4514  zfrepclf  4569  dfid3  4801  oprabbid  6350  axrepndlem1  8988  axrepndlem2  8989  axrepnd  8990  axpowndlem2  8994  axpowndlem2OLD  8995  axpowndlem3  8996  axpowndlem3OLD  8997  axpowndlem4  8998  axregnd  9002  axregndOLD  9003  axinfndlem1  9004  axinfnd  9005  axacndlem4  9009  axacndlem5  9010  axacnd  9011  opabdm  27464  opabrn  27465  pm14.122b  31330  pm14.123b  31333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617
  Copyright terms: Public domain W3C validator