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  5695  funimass4  5697  fconstfvm  5873  fliftel  5937  fliftf  5943  f1oiso  5970  releldm2  6351  frecabcl  6568  qsinxp  6783  qliftel  6787  supisolem  7210  enumctlemm  7316  ismkvnex  7357  genpassl  7747  genpassu  7748  addcomprg  7801  mulcomprg  7803  1idprl  7813  1idpru  7814  archrecnq  7886  archrecpr  7887  caucvgprprlemexbt  7929  caucvgprprlemexb  7930  archsr  8005  map2psrprg  8028  suplocsrlempr  8030  axsuploc  8255  cnegexlem3  8359  cnegex2  8361  recexre  8761  rerecclap  8913  creur  9142  creui  9143  nndiv  9187  arch  9402  nnrecl  9403  expnlbnd  10930  fimaxq  11095  wrdval  11123  clim2  11864  clim2c  11865  clim0c  11867  climabs0  11888  climrecvg1n  11929  sumeq2  11940  mertensabs  12119  prodeq2  12139  zproddc  12161  nndivides  12379  alzdvds  12436  oddm1even  12457  oddnn02np1  12462  oddge22np1  12463  evennn02n  12464  evennn2n  12465  divalgb  12507  modremain  12511  modprmn0modprm0  12850  pythagtriplem2  12860  pythagtrip  12877  pceu  12889  4sqlem12  12996  gsumpropd2  13497  mndpfo  13542  mndpropd  13544  grppropd  13621  conjnmzb  13888  dvdsr02  14141  crngunit  14147  dvdsrpropdg  14183  cnfldui  14625  znunit  14695  iscnp3  14954  lmbrf  14966  cncnp  14981  lmss  14997  metrest  15257  metcnp  15263  metcnp2  15264  txmetcnp  15269  cdivcncfap  15355  ivthdec  15395  lgsquadlem2  15834  2lgslem1a  15844  pw1nct  16663