Theorem rexbidva 2365

Description: Formula-building rule for restricted existential quantifier (deduction rule). (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 1461	. 2 |- F/ x ph
2		ralbidva.1	. 2 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	1, 2	rexbida 2363	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   e. wcel 1433   E.wrex 2349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-rex 2354

This theorem is referenced by:  2rexbiia  2382  2rexbidva  2389  rexeqbidva  2564  dfimafn  5243  funimass4  5245  fconstfvm  5400  fliftel  5453  fliftf  5459  f1oiso  5485  releldm2  5831  qsinxp  6205  qliftel  6209  supisolem  6421  genpassl  6714  genpassu  6715  addcomprg  6768  mulcomprg  6770  1idprl  6780  1idpru  6781  archrecnq  6853  archrecpr  6854  caucvgprprlemexbt  6896  caucvgprprlemexb  6897  archsr  6958  cnegexlem3  7285  cnegex2  7287  recexre  7678  rerecclap  7818  creur  8036  creui  8037  nndiv  8079  arch  8285  nnrecl  8286  expnlbnd  9597  clim2  10122  clim2c  10123  clim0c  10125  climabs0  10146  climrecvg1n  10185  nndivides  10202  alzdvds  10254  oddm1even  10274  oddnn02np1  10280  oddge22np1  10281  evennn02n  10282  evennn2n  10283  divalgb  10325  modremain  10329