Theorem rexbidva 2539

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 2537	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

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

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 2526

This theorem is referenced by:  2rexbiia  2558  2rexbidva  2565  rexeqbidva  2760  dfimafn  5725  funimass4  5727  fconstfvm  5902  fliftel  5966  fliftf  5972  f1oiso  5999  releldm2  6379  frecabcl  6630  qsinxp  6845  qliftel  6849  supisolem  7299  enumctlemm  7405  ismkvnex  7446  genpassl  7839  genpassu  7840  addcomprg  7893  mulcomprg  7895  1idprl  7905  1idpru  7906  archrecnq  7978  archrecpr  7979  caucvgprprlemexbt  8021  caucvgprprlemexb  8022  archsr  8097  map2psrprg  8120  suplocsrlempr  8122  axsuploc  8346  cnegexlem3  8450  cnegex2  8452  recexre  8852  rerecclap  9004  creur  9233  creui  9234  nndiv  9278  arch  9493  nnrecl  9494  expnlbnd  11026  fimaxq  11194  wrdval  11227  clim2  11968  clim2c  11969  clim0c  11971  climabs0  11992  climrecvg1n  12033  sumeq2  12044  mertensabs  12223  prodeq2  12243  zproddc  12265  nndivides  12483  alzdvds  12540  oddm1even  12561  oddnn02np1  12566  oddge22np1  12567  evennn02n  12568  evennn2n  12569  divalgb  12611  modremain  12615  modprmn0modprm0  12954  pythagtriplem2  12964  pythagtrip  12981  pceu  12993  4sqlem12  13100  gsumpropd2  13606  mndpfo  13651  mndpropd  13653  grppropd  13730  conjnmzb  13997  dvdsr02  14250  crngunit  14256  dvdsrpropdg  14292  cnfldui  14737  znunit  14807  iscnp3  15068  lmbrf  15080  cncnp  15095  lmss  15111  metrest  15371  metcnp  15377  metcnp2  15378  txmetcnp  15383  cdivcncfap  15469  ivthdec  15509  lgsquadlem2  15951  2lgslem1a  15961  pw1nct  16777