Theorem rexbidv 2543

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

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-rex 2526

This theorem is referenced by:  rexbii  2549  2rexbidv  2567  rexralbidv  2568  rexeqbi1dv  2754  rexeqbidv  2758  cbvrex2vw  2790  cbvrex2v  2792  rspc2ev  2936  rspc3ev  2938  ceqsrex2v  2949  sbcrext  3120  uniiunlem  3328  eliun  3995  dfiin2g  4024  dfiunv2  4027  nn0suc  4726  rexxpf  4902  elrnmpt  5006  elrnmptg  5009  elimag  5105  funcnvuni  5425  fun11iun  5635  fvelrnb  5724  fvelimab  5733  foco2  5926  elabrex  5930  elabrexg  5931  abrexco  5932  f1oiso  5999  f1oiso2  6000  acexmidlemab  6044  acexmidlemcase  6045  abrexex2g  6313  abrexex2  6317  recseq  6537  tfr0dm  6553  tfr1onlemaccex  6579  tfrcllemsucaccv  6585  tfrcllembxssdm  6587  tfrcllemaccex  6592  tfrcllemres  6593  freceq1  6623  frec0g  6628  freccllem  6633  frecfcllem  6635  frecsuclem  6637  frecsuc  6638  nnaordex  6761  qseq2  6818  elqsg  6819  elixpsn  6970  ixpsnf1o  6971  isfi  7000  enfi  7128  fimax2gtri  7159  elfi  7258  supeq3  7281  supmoti  7284  suplubti  7291  supisolem  7299  cnvinfex  7309  eqinfti  7311  infvalti  7313  infglbti  7316  enomnilem  7429  finomni  7431  exmidomni  7433  fodjum  7437  fodju0  7438  fodjuomnilemres  7439  fodjuomni  7440  ismkvnex  7446  fodjumkvlemres  7450  fodjumkv  7451  enmkvlem  7452  ltexnqq  7723  elinp  7789  prnmaxl  7803  prnminu  7804  prarloclem3  7812  ltdfpr  7821  genpdflem  7822  genipv  7824  genpassl  7839  genpassu  7840  ltexprlemm  7915  ltexprlemloc  7922  cauappcvgprlemm  7960  cauappcvgprlemopl  7961  cauappcvgprlemlol  7962  cauappcvgprlemopu  7963  cauappcvgprlemupu  7964  cauappcvgprlemdisj  7966  cauappcvgprlemloc  7967  cauappcvgprlemladdfu  7969  cauappcvgprlemladdfl  7970  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  cauappcvgprlem1  7974  cauappcvgprlem2  7975  caucvgprlemm  7983  caucvgprlemopl  7984  caucvgprlemlol  7985  caucvgprlemopu  7986  caucvgprlemupu  7987  caucvgprlemdisj  7989  caucvgprlemloc  7990  caucvgprlemladdfu  7992  caucvgprlemladdrl  7993  caucvgprlem1  7994  caucvgprlem2  7995  caucvgprprlemell  8000  caucvgprprlemelu  8001  caucvgprprlemml  8009  caucvgprprlemmu  8010  caucvgprprlemexbt  8021  caucvgprprlem2  8025  suplocexprlemmu  8033  suplocexprlemru  8034  suplocexprlemdisj  8035  suplocexprlemloc  8036  suplocexprlemub  8038  recexgt0sr  8088  archsr  8097  map2psrprg  8120  suplocsrlemb  8121  axprecex  8195  nntopi  8209  axpre-suploclemres  8216  axpre-suploc  8217  cnegex  8451  apreap  8861  recexap  8927  sup3exmid  9231  creur  9233  creui  9234  cju  9235  supinfneg  9927  infsupneg  9928  infssuzex  10593  nninfdcex  10597  exbtwnzlemshrink  10608  rebtwn2zlemshrink  10613  modqmuladd  10728  hashunlem  11168  iswrd  11226  csbwrdg  11254  shftfvalg  11503  shftfval  11506  rexfiuz  11674  recvguniq  11680  fimaxre2  11912  clim  11966  sumeq1  12040  summodc  12069  fsum3  12073  mertenslemub  12220  mertenslemi1  12221  mertenslem2  12222  mertensabs  12223  prodeq1f  12238  prodeq2w  12242  prodmodc  12264  fprodseq  12269  divides  12475  odd2np1lem  12558  opeo  12583  omeo  12584  divalglemeunn  12607  divalglemeuneg  12609  zeqzmulgcd  12666  bezoutlemnewy  12692  bezoutlemmain  12694  bezoutlemex  12697  bezoutlemaz  12699  exprmfct  12835  nnnn0modprm0  12953  pceu  12993  pcprmpw2  13031  4sqlemafi  13093  4sqexercise1  13096  4sqlem12  13100  ennnfoneleminc  13162  ennnfonelemex  13165  ennnfonelemhom  13166  ennnfonelemnn0  13173  ennnfonelemr  13174  ctinfomlemom  13178  ctinfom  13179  nninfdclemcl  13199  nninfdclemp1  13201  nninfdc  13204  ptex  13477  grpinvalem  13598  igsumvalx  13602  gsumpropd  13605  gsumress  13608  gsum0g  13609  isnsgrp  13619  grpinvex  13723  dfgrp2  13740  grpidinv2  13771  grpidinv  13772  dfgrp3mlem  13811  grp1  13819  imasgrp2  13827  dvdsrd  14239  opprunitd  14255  subrgdvds  14380  lss1d  14531  lspsn  14564  ellspsn  14565  rspsn  14682  znf1o  14799  basis2  14913  eltg2  14918  tg2  14925  neival  15008  isnei  15009  isneip  15011  restbasg  15033  cnpval  15063  iscnp  15064  icnpimaex  15076  lmbr  15078  lmbr2  15079  cnptoprest2  15105  lmff  15114  txbas  15123  txcnp  15136  txrest  15141  blssps  15292  blss  15293  mopni  15347  metss  15359  metrest  15371  metcnp3  15376  divcnap  15430  cncfval  15437  elcncf2  15439  cncfmet  15457  dedekindeulemuub  15482  dedekindeulemloc  15484  dedekindeulemlu  15486  suplociccreex  15489  dedekindicclemuub  15491  dedekindicclemloc  15493  dedekindicclemlu  15495  ivthreinc  15510  limccl  15524  ellimc3apf  15525  limcdifap  15527  limcmpted  15528  plyval  15597  elply2  15600  2lgslem1b  15962  upgredg2vtx  16143  usgredg4  16210  ushgredgedg  16221  ushgredgedgloop  16223  vtxd0nedgbfi  16294  bj-inf2vnlem1  16740  bj-inf2vnlem2  16741  bj-nn0sucALT  16748  sscoll2  16758  3dom  16762  subctctexmid  16774  pw1nct  16777  isomninnlem  16814  trilpolemlt1  16825  trirec0  16828  qdiff  16833  ismkvnnlem  16837