ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rexbidv Structured version   Unicode version

Theorem rexbidv 2321
Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)
Hypothesis
Ref Expression
ralbidv.1
Assertion
Ref Expression
rexbidv
Distinct variable group:   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem rexbidv
StepHypRef Expression
1 nfv 1418 . 2  F/
2 ralbidv.1 . 2
31, 2rexbid 2319 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98  wrex 2301
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-rex 2306
This theorem is referenced by:  rexbii  2325  2rexbidv  2343  rexralbidv  2344  rexeqbi1dv  2508  rexeqbidv  2512  cbvrex2v  2536  rspc2ev  2658  rspc3ev  2660  ceqsrex2v  2670  sbcrext  2829  sbcrexg  2831  uniiunlem  3022  eliun  3652  dfiin2g  3681  dfiunv2  3684  nn0suc  4270  rexxpf  4426  elrnmpt  4526  elrnmptg  4529  elimag  4615  funcnvuni  4911  fun11iun  5090  fvelrnb  5164  fvelimab  5172  foelrn  5260  foco2  5261  elabrex  5340  abrexco  5341  f1oiso  5408  f1oiso2  5409  acexmidlemab  5449  acexmidlemcase  5450  grprinvlem  5637  abrexex2g  5689  abrexex2  5693  recseq  5862  tfr0  5878  freceq1  5919  frec0g  5922  frecsuclem3  5929  frecsuc  5930  nnaordex  6036  qseq2  6091  elqsg  6092  isfi  6177  enfi  6252  ltexnqq  6391  elinp  6457  prnmaxl  6471  prnminu  6472  prarloclem3  6480  ltdfpr  6489  genpdflem  6490  genipv  6492  genpassl  6507  genpassu  6508  ltexprlemm  6574  ltexprlemloc  6581  cauappcvgprlemm  6617  cauappcvgprlemopl  6618  cauappcvgprlemlol  6619  cauappcvgprlemopu  6620  cauappcvgprlemupu  6621  cauappcvgprlemdisj  6623  cauappcvgprlemloc  6624  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  cauappcvgprlem1  6631  cauappcvgprlem2  6632  caucvgprlemm  6639  caucvgprlemopl  6640  caucvgprlemlol  6641  caucvgprlemopu  6642  caucvgprlemupu  6643  caucvgprlemdisj  6645  caucvgprlemloc  6646  caucvgprlemladdfu  6648  caucvgprlemladdrl  6649  caucvgprlem1  6650  caucvgprlem2  6651  recexgt0sr  6701  archsr  6708  axprecex  6764  cnegex  6986  apreap  7371  recexap  7416  creur  7692  creui  7693  cju  7694  bj-inf2vnlem1  9430  bj-inf2vnlem2  9431  bj-nn0sucALT  9438
  Copyright terms: Public domain W3C validator