Theorem rexbidva 2530

Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 9-Mar-1997.)

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

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem rexbidva

Step	Hyp	Ref	Expression
1		nfv 1577	. 2 |- F/ x ph
2		ralbidva.1	. 2 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	1, 2	rexbida 2528	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   e. wcel 2202   E.wrex 2512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-rex 2517

This theorem is referenced by:  2rexbiia  2549  2rexbidva  2556  rexeqbidva  2750  dfimafn  5703  funimass4  5705  fconstfvm  5880  fliftel  5944  fliftf  5950  f1oiso  5977  releldm2  6357  frecabcl  6608  qsinxp  6823  qliftel  6827  supisolem  7267  enumctlemm  7373  ismkvnex  7414  genpassl  7804  genpassu  7805  addcomprg  7858  mulcomprg  7860  1idprl  7870  1idpru  7871  archrecnq  7943  archrecpr  7944  caucvgprprlemexbt  7986  caucvgprprlemexb  7987  archsr  8062  map2psrprg  8085  suplocsrlempr  8087  axsuploc  8311  cnegexlem3  8415  cnegex2  8417  recexre  8817  rerecclap  8969  creur  9198  creui  9199  nndiv  9243  arch  9458  nnrecl  9459  expnlbnd  10989  fimaxq  11154  wrdval  11182  clim2  11923  clim2c  11924  clim0c  11926  climabs0  11947  climrecvg1n  11988  sumeq2  11999  mertensabs  12178  prodeq2  12198  zproddc  12220  nndivides  12438  alzdvds  12495  oddm1even  12516  oddnn02np1  12521  oddge22np1  12522  evennn02n  12523  evennn2n  12524  divalgb  12566  modremain  12570  modprmn0modprm0  12909  pythagtriplem2  12919  pythagtrip  12936  pceu  12948  4sqlem12  13055  gsumpropd2  13556  mndpfo  13601  mndpropd  13603  grppropd  13680  conjnmzb  13947  dvdsr02  14200  crngunit  14206  dvdsrpropdg  14242  cnfldui  14685  znunit  14755  iscnp3  15014  lmbrf  15026  cncnp  15041  lmss  15057  metrest  15317  metcnp  15323  metcnp2  15324  txmetcnp  15329  cdivcncfap  15415  ivthdec  15455  lgsquadlem2  15897  2lgslem1a  15907  pw1nct  16725