Theorem rexbidva 2474

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

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

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-rex 2461

This theorem is referenced by:  2rexbiia  2493  2rexbidva  2500  rexeqbidva  2688  dfimafn  5565  funimass4  5567  fconstfvm  5735  fliftel  5794  fliftf  5800  f1oiso  5827  releldm2  6186  frecabcl  6400  qsinxp  6611  qliftel  6615  supisolem  7007  enumctlemm  7113  ismkvnex  7153  genpassl  7523  genpassu  7524  addcomprg  7577  mulcomprg  7579  1idprl  7589  1idpru  7590  archrecnq  7662  archrecpr  7663  caucvgprprlemexbt  7705  caucvgprprlemexb  7706  archsr  7781  map2psrprg  7804  suplocsrlempr  7806  axsuploc  8030  cnegexlem3  8134  cnegex2  8136  recexre  8535  rerecclap  8687  creur  8916  creui  8917  nndiv  8960  arch  9173  nnrecl  9174  expnlbnd  10645  fimaxq  10807  clim2  11291  clim2c  11292  clim0c  11294  climabs0  11315  climrecvg1n  11356  sumeq2  11367  mertensabs  11545  prodeq2  11565  zproddc  11587  nndivides  11804  alzdvds  11860  oddm1even  11880  oddnn02np1  11885  oddge22np1  11886  evennn02n  11887  evennn2n  11888  divalgb  11930  modremain  11934  modprmn0modprm0  12256  pythagtriplem2  12266  pythagtrip  12283  pceu  12295  mndpfo  12839  mndpropd  12841  grppropd  12893  dvdsr02  13274  crngunit  13280  dvdsrpropdg  13316  iscnp3  13706  lmbrf  13718  cncnp  13733  lmss  13749  metrest  14009  metcnp  14015  metcnp2  14016  txmetcnp  14021  cdivcncfap  14090  ivthdec  14125  pw1nct  14755