Theorem rexbidva 2547

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

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

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-rex 2534

This theorem is referenced by:  2rexbiia  2566  2rexbidva  2573  rexeqbidva  2768  dfimafn  5745  funimass4  5747  fconstfvm  5924  dfimafnf  5945  fliftel  5989  fliftf  5995  f1oiso  6022  releldm2  6409  frecabcl  6660  qsinxp  6875  qliftel  6879  supisolem  7338  enumctlemm  7444  ismkvnex  7485  genpassl  7881  genpassu  7882  addcomprg  7935  mulcomprg  7937  1idprl  7947  1idpru  7948  archrecnq  8020  archrecpr  8021  caucvgprprlemexbt  8063  caucvgprprlemexb  8064  archsr  8139  map2psrprg  8162  suplocsrlempr  8164  axsuploc  8388  cnegexlem3  8493  cnegex2  8495  recexre  8896  rerecclap  9050  creur  9279  creui  9280  nndiv  9324  arch  9539  nnrecl  9540  expnlbnd  11080  fimaxq  11248  wrdval  11285  clim2  12027  clim2c  12028  clim0c  12030  climabs0  12051  climrecvg1n  12092  sumeq2  12103  mertensabs  12282  prodeq2  12302  zproddc  12324  nndivides  12542  alzdvds  12599  oddm1even  12620  oddnn02np1  12625  oddge22np1  12626  evennn02n  12627  evennn2n  12628  divalgb  12670  modremain  12674  modprmn0modprm0  13013  pythagtriplem2  13023  pythagtrip  13040  pceu  13052  4sqlem12  13159  ballotfilemsima  13237  mndpfo  13728  mndpropd  13730  grppropd  13799  conjnmzb  14060  dvdsr02  14385  crngunit  14391  dvdsrpropdg  14427  cnfldui  14896  znunit  14966  iscnp3  15227  lmbrf  15239  cncnp  15254  lmss  15270  metrest  15530  metcnp  15536  metcnp2  15537  txmetcnp  15542  cdivcncfap  15628  ivthdec  15668  lgsquadlem2  16111  2lgslem1a  16121  pw1nct  16947