Theorem rexbidva 2503

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

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-rex 2490

This theorem is referenced by:  2rexbiia  2522  2rexbidva  2529  rexeqbidva  2721  dfimafn  5629  funimass4  5631  fconstfvm  5804  fliftel  5864  fliftf  5870  f1oiso  5897  releldm2  6273  frecabcl  6487  qsinxp  6700  qliftel  6704  supisolem  7112  enumctlemm  7218  ismkvnex  7259  genpassl  7639  genpassu  7640  addcomprg  7693  mulcomprg  7695  1idprl  7705  1idpru  7706  archrecnq  7778  archrecpr  7779  caucvgprprlemexbt  7821  caucvgprprlemexb  7822  archsr  7897  map2psrprg  7920  suplocsrlempr  7922  axsuploc  8147  cnegexlem3  8251  cnegex2  8253  recexre  8653  rerecclap  8805  creur  9034  creui  9035  nndiv  9079  arch  9294  nnrecl  9295  expnlbnd  10811  fimaxq  10974  wrdval  10999  clim2  11627  clim2c  11628  clim0c  11630  climabs0  11651  climrecvg1n  11692  sumeq2  11703  mertensabs  11881  prodeq2  11901  zproddc  11923  nndivides  12141  alzdvds  12198  oddm1even  12219  oddnn02np1  12224  oddge22np1  12225  evennn02n  12226  evennn2n  12227  divalgb  12269  modremain  12273  modprmn0modprm0  12612  pythagtriplem2  12622  pythagtrip  12639  pceu  12651  4sqlem12  12758  gsumpropd2  13258  mndpfo  13303  mndpropd  13305  grppropd  13382  conjnmzb  13649  dvdsr02  13900  crngunit  13906  dvdsrpropdg  13942  cnfldui  14384  znunit  14454  iscnp3  14708  lmbrf  14720  cncnp  14735  lmss  14751  metrest  15011  metcnp  15017  metcnp2  15018  txmetcnp  15023  cdivcncfap  15109  ivthdec  15149  lgsquadlem2  15588  2lgslem1a  15598  pw1nct  15977