Theorem rexbidva 2527

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

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

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-rex 2514

This theorem is referenced by:  2rexbiia  2546  2rexbidva  2553  rexeqbidva  2747  dfimafn  5682  funimass4  5684  fconstfvm  5857  fliftel  5917  fliftf  5923  f1oiso  5950  releldm2  6331  frecabcl  6545  qsinxp  6758  qliftel  6762  supisolem  7175  enumctlemm  7281  ismkvnex  7322  genpassl  7711  genpassu  7712  addcomprg  7765  mulcomprg  7767  1idprl  7777  1idpru  7778  archrecnq  7850  archrecpr  7851  caucvgprprlemexbt  7893  caucvgprprlemexb  7894  archsr  7969  map2psrprg  7992  suplocsrlempr  7994  axsuploc  8219  cnegexlem3  8323  cnegex2  8325  recexre  8725  rerecclap  8877  creur  9106  creui  9107  nndiv  9151  arch  9366  nnrecl  9367  expnlbnd  10886  fimaxq  11049  wrdval  11074  clim2  11794  clim2c  11795  clim0c  11797  climabs0  11818  climrecvg1n  11859  sumeq2  11870  mertensabs  12048  prodeq2  12068  zproddc  12090  nndivides  12308  alzdvds  12365  oddm1even  12386  oddnn02np1  12391  oddge22np1  12392  evennn02n  12393  evennn2n  12394  divalgb  12436  modremain  12440  modprmn0modprm0  12779  pythagtriplem2  12789  pythagtrip  12806  pceu  12818  4sqlem12  12925  gsumpropd2  13426  mndpfo  13471  mndpropd  13473  grppropd  13550  conjnmzb  13817  dvdsr02  14069  crngunit  14075  dvdsrpropdg  14111  cnfldui  14553  znunit  14623  iscnp3  14877  lmbrf  14889  cncnp  14904  lmss  14920  metrest  15180  metcnp  15186  metcnp2  15187  txmetcnp  15192  cdivcncfap  15278  ivthdec  15318  lgsquadlem2  15757  2lgslem1a  15767  pw1nct  16369