Theorem rexbidva 1663

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 973	. 2 |- (ph -> A.xph)
2		ralbidva.1	. 2 |- ((ph /\ x e. A) -> (ps <-> ch))
3	1, 2	rexbida 1661	1 |- (ph -> (E.x e. A ps <-> E.x e. A ch))

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

This theorem is referenced by:  2rexbiia 1678  2rexbidva 1682  weinxp 3240  dfimafn 3768  funimass4 3770  fvelimab 3772  fconstfv 3856  isomin 3906  f1oiso 3911  oaass 4202  r1pwcl 4704  brdom7disj 4821  brdom6disj 4822  cnegextlem3 5366  axsup 5526  sup3 6061  infm3 6063  infmsup 6077  nnreclt 6081  supxrre 6092  supxrbnd 6100  supxrbnd1 6104  supxrbnd2 6105  expnlbndt 6663  cau2 6920  sumeq2 6992  infcvglem1 7228  qdensere 7755  iscnp2 7765  cncnplem4 7781  blrn3 7851  metcnplem 7890  metcnp3 7900  iscauf 7943  iscau5 7945  iscaunns 7948  causs 7959  cncms 8002  bcthlem21 8023  nmounbi 8442  nmo0 8454  minveclem28 8575  efifolem7 8730  hcau2 9057  hhcms 9074  hhsscms 9152  projlem1 9188  projlem2 9189  projlem26 9213  pjtheu2 9252  shsel3t 9281  branmfnt 10040  pjima 10106  chrelat 10294  cdj3lem3 10368  cdj3lem3b 10370  fgsb 10563  fgsb2 10568

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-rex 1653

Copyright terms: Public domain