Theorem rexbidva 2120

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

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   e. wcel 1300  E.wrex 2106

This theorem is referenced by:  2rexbiia 2135  2rexbidva 2139  weinxp 4059  dfimafn 4720  funimass4 4722  fvelimabOLD 4726  fconstfv 4825  isomin 4876  f1oiso 4881  oaass 5243  r1pwcl 5798  brdom7disj 5966  brdom6disj 5967  cnegexlem3 6501  axsup 6676  sup3 7261  infm3 7263  infmsup 7277  nnrecl 7281  supxrre 7292  supxrbnd 7300  supxrbnd1 7304  supxrbnd2 7305  expnlbnd 7902  cau2i 8165  sumeq2 8245  infcvglem1 8482  qdensere 9027  iscnp2 9037  cncnplem4 9054  blrn3 9124  metcnplem 9164  metcnp3 9174  iscauf 9217  iscau5 9219  iscaunns 9222  causs 9233  cncms 9276  bcthlem21 9297  nmounbi 9778  nmo0 9791  minveclem28 9917  efifolem7 10082  hcau2 10688  hhcms 10705  hhsscms 10783  projlem1 10819  projlem2 10820  projlem26 10844  pjtheu2i 10883  shsel3 10912  branmfn 11675  branmfnOLD 11676  pjimai 11748  chrelati 11936  cdj3lem3 12010  cdj3lem3b 12012  alzdvds 13695  divalglem4 13699  repcpwti 14503  prl2 14514  prjmapcp2 14515  nZdef 14527  dfdir2 14639  prodeq2 14661  prsubrtr 14763  osneisi 14875  fgsb 14921  fgsb2 14925  bwt2 14960  lvsovso2 15039  supnuf 15041  supexr 15043  vtarsuelt 15272  fictb 15371  isnrm2 15552  geomcau 15849  heiborlem8 15962  isdivrng2 16111  strdif 16719  hlrelat5 17050  hlrelat 17051  cvrat42 17077  polval2 17319

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-rex 2110

Copyright terms: Public domain