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  5684  funimass4  5686  fconstfvm  5861  fliftel  5923  fliftf  5929  f1oiso  5956  releldm2  6337  frecabcl  6551  qsinxp  6766  qliftel  6770  supisolem  7186  enumctlemm  7292  ismkvnex  7333  genpassl  7722  genpassu  7723  addcomprg  7776  mulcomprg  7778  1idprl  7788  1idpru  7789  archrecnq  7861  archrecpr  7862  caucvgprprlemexbt  7904  caucvgprprlemexb  7905  archsr  7980  map2psrprg  8003  suplocsrlempr  8005  axsuploc  8230  cnegexlem3  8334  cnegex2  8336  recexre  8736  rerecclap  8888  creur  9117  creui  9118  nndiv  9162  arch  9377  nnrecl  9378  expnlbnd  10898  fimaxq  11062  wrdval  11087  clim2  11810  clim2c  11811  clim0c  11813  climabs0  11834  climrecvg1n  11875  sumeq2  11886  mertensabs  12064  prodeq2  12084  zproddc  12106  nndivides  12324  alzdvds  12381  oddm1even  12402  oddnn02np1  12407  oddge22np1  12408  evennn02n  12409  evennn2n  12410  divalgb  12452  modremain  12456  modprmn0modprm0  12795  pythagtriplem2  12805  pythagtrip  12822  pceu  12834  4sqlem12  12941  gsumpropd2  13442  mndpfo  13487  mndpropd  13489  grppropd  13566  conjnmzb  13833  dvdsr02  14085  crngunit  14091  dvdsrpropdg  14127  cnfldui  14569  znunit  14639  iscnp3  14893  lmbrf  14905  cncnp  14920  lmss  14936  metrest  15196  metcnp  15202  metcnp2  15203  txmetcnp  15208  cdivcncfap  15294  ivthdec  15334  lgsquadlem2  15773  2lgslem1a  15783  pw1nct  16456