Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem rexbidva 1652

Description: Formula-building rule for restricted existential quantifier (deduction rule).

Hypothesis

Ref	Expression
ralbidva.1

Assertion

Ref	Expression
rexbidva

Distinct variable group:   ,

---

Proof of Theorem rexbidva

Step	Hyp	Ref	Expression
1		ax-17 968	. 2
2		ralbidva.1	. 2
3	1, 2	rexbida 1650	1

Colors of variables: wff set class

Syntax hints:   wi 3   wb 146   wa 223   wcel 955  wrex 1638

This theorem is referenced by:  2rexbiia 1667  2rexbidva 1671  weinxp 3223  dfimafn 3746  funimass4 3748  fvelimab 3750  fconstfv 3834  isomin 3884  f1oiso 3889  oaass 4179  r1pwcl 4659  brdom7disj 4776  brdom6disj 4777  cnegextlem3 5319  axsup 5479  sup3 5999  infm3 6001  infmsup 6015  nnreclt 6019  supxrre 6030  supxrbnd 6038  supxrbnd1 6042  supxrbnd2 6043  cau2 6850  sumeq2 6923  infcvglem1 7156  qdensere 7691  cncnplem4 7716  blrn3 7787  metcnplem 7825  metcnp3 7835  iscauf 7877  iscau5 7878  causs 7890  cncms 7932  bcthlem21 7953  nmounbi 8371  nmo0 8383  minveclem28 8503  efifolem7 8643  hcau2 8976  hhcms 8993  hhsscms 9067  projlem1 9102  projlem2 9103  projlem26 9127  pjtheu2 9165  shsel3t 9194  branmfnt 9951  pjima 10015  chrelat 10199  cdj3lem3 10270  cdj3lem3b 10272  fgsb 10444  fgsb2 10449

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-rex 1642

Copyright terms: Public domain