Theorem rexbidva 1657

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

Hypothesis

Ref	Expression
ralbidva.1	|- ((ph /\ x e. A) -> (ps <-> ch))

Assertion

Ref	Expression
rexbidva	|- (ph -> (E.x e. A ps <-> E.x e. A ch))

Distinct variable group:   ph,x

Proof of Theorem rexbidva

Step	Hyp	Ref	Expression
1		ax-17 969	. 2 |- (ph -> A.xph)
2		ralbidva.1	. 2 |- ((ph /\ x e. A) -> (ps <-> ch))
3	1, 2	rexbida 1655	1 |- (ph -> (E.x e. A ps <-> E.x e. A ch))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   e. wcel 956  E.wrex 1643

This theorem is referenced by:  2rexbiia 1672  2rexbidva 1676  weinxp 3228  dfimafn 3752  funimass4 3754  fvelimab 3756  fconstfv 3840  isomin 3890  f1oiso 3895  oaass 4185  r1pwcl 4667  brdom7disj 4784  brdom6disj 4785  cnegextlem3 5327  axsup 5487  sup3 6007  infm3 6009  infmsup 6023  nnreclt 6027  supxrre 6038  supxrbnd 6046  supxrbnd1 6050  supxrbnd2 6051  cau2 6858  sumeq2 6931  infcvglem1 7164  qdensere 7701  iscnp2 7711  cncnplem4 7727  blrn3 7799  metcnplem 7838  metcnp3 7848  iscauf 7891  iscau5 7893  causs 7906  cncms 7948  bcthlem21 7969  nmounbi 8384  nmo0 8396  minveclem28 8516  efifolem7 8662  hcau2 8994  hhcms 9011  hhsscms 9089  projlem1 9125  projlem2 9126  projlem26 9150  pjtheu2 9188  shsel3t 9217  branmfnt 9976  pjima 10042  chrelat 10228  cdj3lem3 10299  cdj3lem3b 10301  fgsb 10480  fgsb2 10485

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-rex 1647

Copyright terms: Public domain