Theorem rexbidva 2494

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

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-rex 2481

This theorem is referenced by:  2rexbiia  2513  2rexbidva  2520  rexeqbidva  2712  dfimafn  5612  funimass4  5614  fconstfvm  5783  fliftel  5843  fliftf  5849  f1oiso  5876  releldm2  6252  frecabcl  6466  qsinxp  6679  qliftel  6683  supisolem  7083  enumctlemm  7189  ismkvnex  7230  genpassl  7608  genpassu  7609  addcomprg  7662  mulcomprg  7664  1idprl  7674  1idpru  7675  archrecnq  7747  archrecpr  7748  caucvgprprlemexbt  7790  caucvgprprlemexb  7791  archsr  7866  map2psrprg  7889  suplocsrlempr  7891  axsuploc  8116  cnegexlem3  8220  cnegex2  8222  recexre  8622  rerecclap  8774  creur  9003  creui  9004  nndiv  9048  arch  9263  nnrecl  9264  expnlbnd  10773  fimaxq  10936  wrdval  10955  clim2  11465  clim2c  11466  clim0c  11468  climabs0  11489  climrecvg1n  11530  sumeq2  11541  mertensabs  11719  prodeq2  11739  zproddc  11761  nndivides  11979  alzdvds  12036  oddm1even  12057  oddnn02np1  12062  oddge22np1  12063  evennn02n  12064  evennn2n  12065  divalgb  12107  modremain  12111  modprmn0modprm0  12450  pythagtriplem2  12460  pythagtrip  12477  pceu  12489  4sqlem12  12596  gsumpropd2  13095  mndpfo  13140  mndpropd  13142  grppropd  13219  conjnmzb  13486  dvdsr02  13737  crngunit  13743  dvdsrpropdg  13779  cnfldui  14221  znunit  14291  iscnp3  14523  lmbrf  14535  cncnp  14550  lmss  14566  metrest  14826  metcnp  14832  metcnp2  14833  txmetcnp  14838  cdivcncfap  14924  ivthdec  14964  lgsquadlem2  15403  2lgslem1a  15413  pw1nct  15734