NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  exbidv Unicode version

Theorem exbidv 1626
Description: Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
albidv.1
Assertion
Ref Expression
exbidv
Distinct variable group:   ,
Allowed substitution hints:   ()   ()

Proof of Theorem exbidv
StepHypRef Expression
1 ax-17 1616 . 2
2 albidv.1 . 2
31, 2exbidh 1591 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wb 176  wex 1541
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616
This theorem depends on definitions:  df-bi 177  df-ex 1542
This theorem is referenced by:  2exbidv  1628  3exbidv  1629  eubid  2211  eleq1  2413  eleq2  2414  rexbidv2  2637  ceqsex2  2895  alexeq  2968  ceqex  2969  sbc2or  3054  sbc5  3070  sbcex2  3095  sbcexg  3096  sbcabel  3123  eluni  3894  csbunig  3899  intab  3956  el1c  4139  opkelopkabg  4245  otkelins3kg  4254  opkelcokg  4261  opkelimagekg  4271  sfineq1  4526  sfineq2  4527  phiall  4618  cbvopab1  4632  cbvopab1s  4634  setconslem6  4736  csbxpg  4813  opeliunxp  4820  br1st  4858  br2nd  4859  brco  4883  dfdmf  4905  dfrnf  4962  csbrng  4966  dfco2a  5081  cores  5084  tz6.12-2  5346  fnrnfv  5364  dmfco  5381  funiunfv  5467  isomin  5496  cbvoprab1  5567  cbvoprab2  5568  oqelins4  5794  txpcofun  5803  erdmrn  5965  mapsn  6026  bren  6030  ce0nnul  6177  ce0ncpw1  6185  dflec3  6221  nclenc  6222  taddc  6229
  Copyright terms: Public domain W3C validator