Theorem rexbidva 2529

Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 9-Mar-1997.)

Hypothesis

Ref	Expression
ralbidva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rexbidva	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rexbidva

Step	Hyp	Ref	Expression
1		nfv 1576	. 2 ⊢ Ⅎ𝑥𝜑
2		ralbidva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	1, 2	rexbida 2527	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∈ wcel 2202  ∃wrex 2511

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-rex 2516

This theorem is referenced by:  2rexbiia  2548  2rexbidva  2555  rexeqbidva  2749  dfimafn  5694  funimass4  5696  fconstfvm  5872  fliftel  5934  fliftf  5940  f1oiso  5967  releldm2  6348  frecabcl  6565  qsinxp  6780  qliftel  6784  supisolem  7207  enumctlemm  7313  ismkvnex  7354  genpassl  7744  genpassu  7745  addcomprg  7798  mulcomprg  7800  1idprl  7810  1idpru  7811  archrecnq  7883  archrecpr  7884  caucvgprprlemexbt  7926  caucvgprprlemexb  7927  archsr  8002  map2psrprg  8025  suplocsrlempr  8027  axsuploc  8252  cnegexlem3  8356  cnegex2  8358  recexre  8758  rerecclap  8910  creur  9139  creui  9140  nndiv  9184  arch  9399  nnrecl  9400  expnlbnd  10927  fimaxq  11092  wrdval  11120  clim2  11848  clim2c  11849  clim0c  11851  climabs0  11872  climrecvg1n  11913  sumeq2  11924  mertensabs  12103  prodeq2  12123  zproddc  12145  nndivides  12363  alzdvds  12420  oddm1even  12441  oddnn02np1  12446  oddge22np1  12447  evennn02n  12448  evennn2n  12449  divalgb  12491  modremain  12495  modprmn0modprm0  12834  pythagtriplem2  12844  pythagtrip  12861  pceu  12873  4sqlem12  12980  gsumpropd2  13481  mndpfo  13526  mndpropd  13528  grppropd  13605  conjnmzb  13872  dvdsr02  14125  crngunit  14131  dvdsrpropdg  14167  cnfldui  14609  znunit  14679  iscnp3  14933  lmbrf  14945  cncnp  14960  lmss  14976  metrest  15236  metcnp  15242  metcnp2  15243  txmetcnp  15248  cdivcncfap  15334  ivthdec  15374  lgsquadlem2  15813  2lgslem1a  15823  pw1nct  16630