Theorem rexbidv 2439

Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 20-Nov-1994.)

Hypothesis

Ref	Expression
ralbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

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

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem rexbidv

Step	Hyp	Ref	Expression
1		nfv 1509	. 2 ⊢ Ⅎ𝑥𝜑
2		ralbidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	rexbid 2437	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 104  ∃wrex 2418

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-rex 2423

This theorem is referenced by:  rexbii  2445  2rexbidv  2463  rexralbidv  2464  rexeqbi1dv  2638  rexeqbidv  2642  cbvrex2v  2669  rspc2ev  2808  rspc3ev  2810  ceqsrex2v  2821  sbcrext  2990  uniiunlem  3190  eliun  3825  dfiin2g  3854  dfiunv2  3857  nn0suc  4526  rexxpf  4694  elrnmpt  4796  elrnmptg  4799  elimag  4893  funcnvuni  5200  fun11iun  5396  fvelrnb  5477  fvelimab  5485  foco2  5663  elabrex  5667  abrexco  5668  f1oiso  5735  f1oiso2  5736  acexmidlemab  5776  acexmidlemcase  5777  grprinvlem  5973  abrexex2g  6026  abrexex2  6030  recseq  6211  tfr0dm  6227  tfr1onlemaccex  6253  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllemaccex  6266  tfrcllemres  6267  freceq1  6297  frec0g  6302  freccllem  6307  frecfcllem  6309  frecsuclem  6311  frecsuc  6312  nnaordex  6431  qseq2  6486  elqsg  6487  elixpsn  6637  ixpsnf1o  6638  isfi  6663  enfi  6775  fimax2gtri  6803  elfi  6867  supeq3  6885  supmoti  6888  suplubti  6895  supisolem  6903  cnvinfex  6913  eqinfti  6915  infvalti  6917  infglbti  6920  enomnilem  7018  finomni  7020  exmidomni  7022  fodjum  7026  fodju0  7027  fodjuomnilemres  7028  fodjuomni  7029  ismkvnex  7037  fodjumkvlemres  7041  fodjumkv  7042  enmkvlem  7043  ltexnqq  7240  elinp  7306  prnmaxl  7320  prnminu  7321  prarloclem3  7329  ltdfpr  7338  genpdflem  7339  genipv  7341  genpassl  7356  genpassu  7357  ltexprlemm  7432  ltexprlemloc  7439  cauappcvgprlemm  7477  cauappcvgprlemopl  7478  cauappcvgprlemlol  7479  cauappcvgprlemopu  7480  cauappcvgprlemupu  7481  cauappcvgprlemdisj  7483  cauappcvgprlemloc  7484  cauappcvgprlemladdfu  7486  cauappcvgprlemladdfl  7487  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  cauappcvgprlem1  7491  cauappcvgprlem2  7492  caucvgprlemm  7500  caucvgprlemopl  7501  caucvgprlemlol  7502  caucvgprlemopu  7503  caucvgprlemupu  7504  caucvgprlemdisj  7506  caucvgprlemloc  7507  caucvgprlemladdfu  7509  caucvgprlemladdrl  7510  caucvgprlem1  7511  caucvgprlem2  7512  caucvgprprlemell  7517  caucvgprprlemelu  7518  caucvgprprlemml  7526  caucvgprprlemmu  7527  caucvgprprlemexbt  7538  caucvgprprlem2  7542  suplocexprlemmu  7550  suplocexprlemru  7551  suplocexprlemdisj  7552  suplocexprlemloc  7553  suplocexprlemub  7555  recexgt0sr  7605  archsr  7614  map2psrprg  7637  suplocsrlemb  7638  axprecex  7712  nntopi  7726  axpre-suploclemres  7733  axpre-suploc  7734  cnegex  7964  apreap  8373  recexap  8438  sup3exmid  8739  creur  8741  creui  8742  cju  8743  supinfneg  9417  infsupneg  9418  exbtwnzlemshrink  10057  rebtwn2zlemshrink  10062  modqmuladd  10170  hashunlem  10582  shftfvalg  10622  shftfval  10625  rexfiuz  10793  recvguniq  10799  fimaxre2  11030  clim  11082  sumeq1  11156  summodc  11184  fsum3  11188  mertenslemub  11335  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  prodeq1f  11353  prodeq2w  11357  prodmodc  11379  fprodseq  11384  divides  11531  odd2np1lem  11605  opeo  11630  omeo  11631  divalglemeunn  11654  divalglemeuneg  11656  infssuzex  11678  zeqzmulgcd  11695  bezoutlemnewy  11720  bezoutlemmain  11722  bezoutlemex  11725  bezoutlemaz  11727  exprmfct  11854  ennnfoneleminc  11960  ennnfonelemex  11963  ennnfonelemhom  11964  ennnfonelemnn0  11971  ennnfonelemr  11972  ctinfomlemom  11976  ctinfom  11977  basis2  12254  eltg2  12261  tg2  12268  neival  12351  isnei  12352  isneip  12354  restbasg  12376  cnpval  12406  iscnp  12407  icnpimaex  12419  lmbr  12421  lmbr2  12422  cnptoprest2  12448  lmff  12457  txbas  12466  txcnp  12479  txrest  12484  blssps  12635  blss  12636  mopni  12690  metss  12702  metrest  12714  metcnp3  12719  divcnap  12763  cncfval  12767  elcncf2  12769  cncfmet  12787  dedekindeulemuub  12803  dedekindeulemloc  12805  dedekindeulemlu  12807  suplociccreex  12810  dedekindicclemuub  12812  dedekindicclemloc  12814  dedekindicclemlu  12816  limccl  12836  ellimc3apf  12837  limcdifap  12839  limcmpted  12840  bj-inf2vnlem1  13339  bj-inf2vnlem2  13340  bj-nn0sucALT  13347  sscoll2  13357  subctctexmid  13369  pw1nct  13371  isomninnlem  13400  trilpolemlt1  13409  trirec0  13412  ismkvnnlem  13419