Theorem rexbidva 2323

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

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98   e. wcel 1393   E.wrex 2307

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-rex 2312

This theorem is referenced by:  2rexbiia  2340  2rexbidva  2347  rexeqbidva  2520  dfimafn  5222  funimass4  5224  fconstfvm  5379  fliftel  5433  fliftf  5439  f1oiso  5465  releldm2  5811  qsinxp  6182  qliftel  6186  genpassl  6622  genpassu  6623  addcomprg  6676  mulcomprg  6678  1idprl  6688  1idpru  6689  archrecnq  6761  archrecpr  6762  caucvgprprlemexbt  6804  caucvgprprlemexb  6805  archsr  6866  cnegexlem3  7188  cnegex2  7190  recexre  7569  rerecclap  7706  creur  7911  creui  7912  nndiv  7954  arch  8178  nnrecl  8179  expnlbnd  9373  clim2  9804  clim2c  9805  clim0c  9807  climabs0  9828  climrecvg1n  9867