Theorem rexbidv 2506

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 1550	. 2 ⊢ Ⅎ𝑥𝜑
2		ralbidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	rexbid 2504	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 105  ∃wrex 2484

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-rex 2489

This theorem is referenced by:  rexbii  2512  2rexbidv  2530  rexralbidv  2531  rexeqbi1dv  2714  rexeqbidv  2718  cbvrex2vw  2749  cbvrex2v  2751  rspc2ev  2891  rspc3ev  2893  ceqsrex2v  2904  sbcrext  3075  uniiunlem  3281  eliun  3930  dfiin2g  3959  dfiunv2  3962  nn0suc  4651  rexxpf  4824  elrnmpt  4926  elrnmptg  4929  elimag  5025  funcnvuni  5342  fun11iun  5542  fvelrnb  5625  fvelimab  5634  foco2  5821  elabrex  5825  elabrexg  5826  abrexco  5827  f1oiso  5894  f1oiso2  5895  acexmidlemab  5937  acexmidlemcase  5938  abrexex2g  6204  abrexex2  6208  recseq  6391  tfr0dm  6407  tfr1onlemaccex  6433  tfrcllemsucaccv  6439  tfrcllembxssdm  6441  tfrcllemaccex  6446  tfrcllemres  6447  freceq1  6477  frec0g  6482  freccllem  6487  frecfcllem  6489  frecsuclem  6491  frecsuc  6492  nnaordex  6613  qseq2  6670  elqsg  6671  elixpsn  6821  ixpsnf1o  6822  isfi  6851  enfi  6969  fimax2gtri  6997  elfi  7072  supeq3  7091  supmoti  7094  suplubti  7101  supisolem  7109  cnvinfex  7119  eqinfti  7121  infvalti  7123  infglbti  7126  enomnilem  7239  finomni  7241  exmidomni  7243  fodjum  7247  fodju0  7248  fodjuomnilemres  7249  fodjuomni  7250  ismkvnex  7256  fodjumkvlemres  7260  fodjumkv  7261  enmkvlem  7262  ltexnqq  7520  elinp  7586  prnmaxl  7600  prnminu  7601  prarloclem3  7609  ltdfpr  7618  genpdflem  7619  genipv  7621  genpassl  7636  genpassu  7637  ltexprlemm  7712  ltexprlemloc  7719  cauappcvgprlemm  7757  cauappcvgprlemopl  7758  cauappcvgprlemlol  7759  cauappcvgprlemopu  7760  cauappcvgprlemupu  7761  cauappcvgprlemdisj  7763  cauappcvgprlemloc  7764  cauappcvgprlemladdfu  7766  cauappcvgprlemladdfl  7767  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  cauappcvgprlem1  7771  cauappcvgprlem2  7772  caucvgprlemm  7780  caucvgprlemopl  7781  caucvgprlemlol  7782  caucvgprlemopu  7783  caucvgprlemupu  7784  caucvgprlemdisj  7786  caucvgprlemloc  7787  caucvgprlemladdfu  7789  caucvgprlemladdrl  7790  caucvgprlem1  7791  caucvgprlem2  7792  caucvgprprlemell  7797  caucvgprprlemelu  7798  caucvgprprlemml  7806  caucvgprprlemmu  7807  caucvgprprlemexbt  7818  caucvgprprlem2  7822  suplocexprlemmu  7830  suplocexprlemru  7831  suplocexprlemdisj  7832  suplocexprlemloc  7833  suplocexprlemub  7835  recexgt0sr  7885  archsr  7894  map2psrprg  7917  suplocsrlemb  7918  axprecex  7992  nntopi  8006  axpre-suploclemres  8013  axpre-suploc  8014  cnegex  8249  apreap  8659  recexap  8725  sup3exmid  9029  creur  9031  creui  9032  cju  9033  supinfneg  9715  infsupneg  9716  infssuzex  10374  nninfdcex  10378  exbtwnzlemshrink  10389  rebtwn2zlemshrink  10394  modqmuladd  10509  hashunlem  10947  iswrd  10994  csbwrdg  11021  shftfvalg  11071  shftfval  11074  rexfiuz  11242  recvguniq  11248  fimaxre2  11480  clim  11534  sumeq1  11608  summodc  11636  fsum3  11640  mertenslemub  11787  mertenslemi1  11788  mertenslem2  11789  mertensabs  11790  prodeq1f  11805  prodeq2w  11809  prodmodc  11831  fprodseq  11836  divides  12042  odd2np1lem  12125  opeo  12150  omeo  12151  divalglemeunn  12174  divalglemeuneg  12176  zeqzmulgcd  12233  bezoutlemnewy  12259  bezoutlemmain  12261  bezoutlemex  12264  bezoutlemaz  12266  exprmfct  12402  nnnn0modprm0  12520  pceu  12560  pcprmpw2  12598  4sqlemafi  12660  4sqexercise1  12663  4sqlem12  12667  ennnfoneleminc  12724  ennnfonelemex  12727  ennnfonelemhom  12728  ennnfonelemnn0  12735  ennnfonelemr  12736  ctinfomlemom  12740  ctinfom  12741  nninfdclemcl  12761  nninfdclemp1  12763  nninfdc  12766  ptex  13038  grpinvalem  13159  igsumvalx  13163  gsumpropd  13166  gsumress  13169  gsum0g  13170  isnsgrp  13180  grpinvex  13284  dfgrp2  13301  grpidinv2  13332  grpidinv  13333  dfgrp3mlem  13372  grp1  13380  imasgrp2  13388  dvdsrd  13798  opprunitd  13814  subrgdvds  13939  lss1d  14087  lspsn  14120  ellspsn  14121  rspsn  14238  znf1o  14355  basis2  14462  eltg2  14467  tg2  14474  neival  14557  isnei  14558  isneip  14560  restbasg  14582  cnpval  14612  iscnp  14613  icnpimaex  14625  lmbr  14627  lmbr2  14628  cnptoprest2  14654  lmff  14663  txbas  14672  txcnp  14685  txrest  14690  blssps  14841  blss  14842  mopni  14896  metss  14908  metrest  14920  metcnp3  14925  divcnap  14979  cncfval  14986  elcncf2  14988  cncfmet  15006  dedekindeulemuub  15031  dedekindeulemloc  15033  dedekindeulemlu  15035  suplociccreex  15038  dedekindicclemuub  15040  dedekindicclemloc  15042  dedekindicclemlu  15044  ivthreinc  15059  limccl  15073  ellimc3apf  15074  limcdifap  15076  limcmpted  15077  plyval  15146  elply2  15149  2lgslem1b  15508  bj-inf2vnlem1  15839  bj-inf2vnlem2  15840  bj-nn0sucALT  15847  sscoll2  15857  subctctexmid  15870  pw1nct  15873  isomninnlem  15902  trilpolemlt1  15913  trirec0  15916  ismkvnnlem  15924