Theorem rexbidva 2371

Description: Formula-building rule for restricted existential quantifier (deduction rule). (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 1462	. 2 ⊢ Ⅎ𝑥𝜑
2		ralbidva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	1, 2	rexbida 2369	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103   ∈ wcel 1434  ∃wrex 2354

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468

This theorem depends on definitions:  df-bi 115  df-nf 1391  df-rex 2359

This theorem is referenced by:  2rexbiia  2388  2rexbidva  2395  rexeqbidva  2570  dfimafn  5298  funimass4  5300  fconstfvm  5455  fliftel  5512  fliftf  5518  f1oiso  5544  releldm2  5890  frecabcl  6096  qsinxp  6298  qliftel  6302  supisolem  6610  genpassl  6986  genpassu  6987  addcomprg  7040  mulcomprg  7042  1idprl  7052  1idpru  7053  archrecnq  7125  archrecpr  7126  caucvgprprlemexbt  7168  caucvgprprlemexb  7169  archsr  7230  cnegexlem3  7562  cnegex2  7564  recexre  7955  rerecclap  8095  creur  8313  creui  8314  nndiv  8356  arch  8562  nnrecl  8563  expnlbnd  9913  clim2  10496  clim2c  10497  clim0c  10499  climabs0  10520  climrecvg1n  10559  sumeq2d  10570  sumeq2  10571  nndivides  10583  alzdvds  10635  oddm1even  10655  oddnn02np1  10660  oddge22np1  10661  evennn02n  10662  evennn2n  10663  divalgb  10705  modremain  10709