Theorem rexbidva 2467

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 1521	. 2 ⊢ Ⅎ𝑥𝜑
2		ralbidva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	1, 2	rexbida 2465	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∈ wcel 2141  ∃wrex 2449

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-rex 2454

This theorem is referenced by:  2rexbiia  2486  2rexbidva  2493  rexeqbidva  2680  dfimafn  5545  funimass4  5547  fconstfvm  5714  fliftel  5772  fliftf  5778  f1oiso  5805  releldm2  6164  frecabcl  6378  qsinxp  6589  qliftel  6593  supisolem  6985  enumctlemm  7091  ismkvnex  7131  genpassl  7486  genpassu  7487  addcomprg  7540  mulcomprg  7542  1idprl  7552  1idpru  7553  archrecnq  7625  archrecpr  7626  caucvgprprlemexbt  7668  caucvgprprlemexb  7669  archsr  7744  map2psrprg  7767  suplocsrlempr  7769  axsuploc  7992  cnegexlem3  8096  cnegex2  8098  recexre  8497  rerecclap  8647  creur  8875  creui  8876  nndiv  8919  arch  9132  nnrecl  9133  expnlbnd  10600  fimaxq  10762  clim2  11246  clim2c  11247  clim0c  11249  climabs0  11270  climrecvg1n  11311  sumeq2  11322  mertensabs  11500  prodeq2  11520  zproddc  11542  nndivides  11759  alzdvds  11814  oddm1even  11834  oddnn02np1  11839  oddge22np1  11840  evennn02n  11841  evennn2n  11842  divalgb  11884  modremain  11888  modprmn0modprm0  12210  pythagtriplem2  12220  pythagtrip  12237  pceu  12249  mndpfo  12674  mndpropd  12676  grppropd  12724  iscnp3  12997  lmbrf  13009  cncnp  13024  lmss  13040  metrest  13300  metcnp  13306  metcnp2  13307  txmetcnp  13312  cdivcncfap  13381  ivthdec  13416  pw1nct  14036