Theorem rexbidva 2505

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

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

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-rex 2492

This theorem is referenced by:  2rexbiia  2524  2rexbidva  2531  rexeqbidva  2724  dfimafn  5650  funimass4  5652  fconstfvm  5825  fliftel  5885  fliftf  5891  f1oiso  5918  releldm2  6294  frecabcl  6508  qsinxp  6721  qliftel  6725  supisolem  7136  enumctlemm  7242  ismkvnex  7283  genpassl  7672  genpassu  7673  addcomprg  7726  mulcomprg  7728  1idprl  7738  1idpru  7739  archrecnq  7811  archrecpr  7812  caucvgprprlemexbt  7854  caucvgprprlemexb  7855  archsr  7930  map2psrprg  7953  suplocsrlempr  7955  axsuploc  8180  cnegexlem3  8284  cnegex2  8286  recexre  8686  rerecclap  8838  creur  9067  creui  9068  nndiv  9112  arch  9327  nnrecl  9328  expnlbnd  10846  fimaxq  11009  wrdval  11034  clim2  11709  clim2c  11710  clim0c  11712  climabs0  11733  climrecvg1n  11774  sumeq2  11785  mertensabs  11963  prodeq2  11983  zproddc  12005  nndivides  12223  alzdvds  12280  oddm1even  12301  oddnn02np1  12306  oddge22np1  12307  evennn02n  12308  evennn2n  12309  divalgb  12351  modremain  12355  modprmn0modprm0  12694  pythagtriplem2  12704  pythagtrip  12721  pceu  12733  4sqlem12  12840  gsumpropd2  13340  mndpfo  13385  mndpropd  13387  grppropd  13464  conjnmzb  13731  dvdsr02  13982  crngunit  13988  dvdsrpropdg  14024  cnfldui  14466  znunit  14536  iscnp3  14790  lmbrf  14802  cncnp  14817  lmss  14833  metrest  15093  metcnp  15099  metcnp2  15100  txmetcnp  15105  cdivcncfap  15191  ivthdec  15231  lgsquadlem2  15670  2lgslem1a  15680  pw1nct  16142