Theorem rexbidv 2531

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

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

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-rex 2514

This theorem is referenced by:  rexbii  2537  2rexbidv  2555  rexralbidv  2556  rexeqbi1dv  2741  rexeqbidv  2745  cbvrex2vw  2777  cbvrex2v  2779  rspc2ev  2923  rspc3ev  2925  ceqsrex2v  2936  sbcrext  3107  uniiunlem  3314  eliun  3972  dfiin2g  4001  dfiunv2  4004  nn0suc  4700  rexxpf  4875  elrnmpt  4979  elrnmptg  4982  elimag  5078  funcnvuni  5396  fun11iun  5601  fvelrnb  5689  fvelimab  5698  foco2  5889  elabrex  5893  elabrexg  5894  abrexco  5895  f1oiso  5962  f1oiso2  5963  acexmidlemab  6007  acexmidlemcase  6008  abrexex2g  6277  abrexex2  6281  recseq  6467  tfr0dm  6483  tfr1onlemaccex  6509  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllemaccex  6522  tfrcllemres  6523  freceq1  6553  frec0g  6558  freccllem  6563  frecfcllem  6565  frecsuclem  6567  frecsuc  6568  nnaordex  6691  qseq2  6748  elqsg  6749  elixpsn  6899  ixpsnf1o  6900  isfi  6929  enfi  7055  fimax2gtri  7084  elfi  7161  supeq3  7180  supmoti  7183  suplubti  7190  supisolem  7198  cnvinfex  7208  eqinfti  7210  infvalti  7212  infglbti  7215  enomnilem  7328  finomni  7330  exmidomni  7332  fodjum  7336  fodju0  7337  fodjuomnilemres  7338  fodjuomni  7339  ismkvnex  7345  fodjumkvlemres  7349  fodjumkv  7350  enmkvlem  7351  ltexnqq  7618  elinp  7684  prnmaxl  7698  prnminu  7699  prarloclem3  7707  ltdfpr  7716  genpdflem  7717  genipv  7719  genpassl  7734  genpassu  7735  ltexprlemm  7810  ltexprlemloc  7817  cauappcvgprlemm  7855  cauappcvgprlemopl  7856  cauappcvgprlemlol  7857  cauappcvgprlemopu  7858  cauappcvgprlemupu  7859  cauappcvgprlemdisj  7861  cauappcvgprlemloc  7862  cauappcvgprlemladdfu  7864  cauappcvgprlemladdfl  7865  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  cauappcvgprlem1  7869  cauappcvgprlem2  7870  caucvgprlemm  7878  caucvgprlemopl  7879  caucvgprlemlol  7880  caucvgprlemopu  7881  caucvgprlemupu  7882  caucvgprlemdisj  7884  caucvgprlemloc  7885  caucvgprlemladdfu  7887  caucvgprlemladdrl  7888  caucvgprlem1  7889  caucvgprlem2  7890  caucvgprprlemell  7895  caucvgprprlemelu  7896  caucvgprprlemml  7904  caucvgprprlemmu  7905  caucvgprprlemexbt  7916  caucvgprprlem2  7920  suplocexprlemmu  7928  suplocexprlemru  7929  suplocexprlemdisj  7930  suplocexprlemloc  7931  suplocexprlemub  7933  recexgt0sr  7983  archsr  7992  map2psrprg  8015  suplocsrlemb  8016  axprecex  8090  nntopi  8104  axpre-suploclemres  8111  axpre-suploc  8112  cnegex  8347  apreap  8757  recexap  8823  sup3exmid  9127  creur  9129  creui  9130  cju  9131  supinfneg  9819  infsupneg  9820  infssuzex  10483  nninfdcex  10487  exbtwnzlemshrink  10498  rebtwn2zlemshrink  10503  modqmuladd  10618  hashunlem  11057  iswrd  11105  csbwrdg  11133  shftfvalg  11369  shftfval  11372  rexfiuz  11540  recvguniq  11546  fimaxre2  11778  clim  11832  sumeq1  11906  summodc  11934  fsum3  11938  mertenslemub  12085  mertenslemi1  12086  mertenslem2  12087  mertensabs  12088  prodeq1f  12103  prodeq2w  12107  prodmodc  12129  fprodseq  12134  divides  12340  odd2np1lem  12423  opeo  12448  omeo  12449  divalglemeunn  12472  divalglemeuneg  12474  zeqzmulgcd  12531  bezoutlemnewy  12557  bezoutlemmain  12559  bezoutlemex  12562  bezoutlemaz  12564  exprmfct  12700  nnnn0modprm0  12818  pceu  12858  pcprmpw2  12896  4sqlemafi  12958  4sqexercise1  12961  4sqlem12  12965  ennnfoneleminc  13022  ennnfonelemex  13025  ennnfonelemhom  13026  ennnfonelemnn0  13033  ennnfonelemr  13034  ctinfomlemom  13038  ctinfom  13039  nninfdclemcl  13059  nninfdclemp1  13061  nninfdc  13064  ptex  13337  grpinvalem  13458  igsumvalx  13462  gsumpropd  13465  gsumress  13468  gsum0g  13469  isnsgrp  13479  grpinvex  13583  dfgrp2  13600  grpidinv2  13631  grpidinv  13632  dfgrp3mlem  13671  grp1  13679  imasgrp2  13687  dvdsrd  14098  opprunitd  14114  subrgdvds  14239  lss1d  14387  lspsn  14420  ellspsn  14421  rspsn  14538  znf1o  14655  basis2  14762  eltg2  14767  tg2  14774  neival  14857  isnei  14858  isneip  14860  restbasg  14882  cnpval  14912  iscnp  14913  icnpimaex  14925  lmbr  14927  lmbr2  14928  cnptoprest2  14954  lmff  14963  txbas  14972  txcnp  14985  txrest  14990  blssps  15141  blss  15142  mopni  15196  metss  15208  metrest  15220  metcnp3  15225  divcnap  15279  cncfval  15286  elcncf2  15288  cncfmet  15306  dedekindeulemuub  15331  dedekindeulemloc  15333  dedekindeulemlu  15335  suplociccreex  15338  dedekindicclemuub  15340  dedekindicclemloc  15342  dedekindicclemlu  15344  ivthreinc  15359  limccl  15373  ellimc3apf  15374  limcdifap  15376  limcmpted  15377  plyval  15446  elply2  15449  2lgslem1b  15808  upgredg2vtx  15987  usgredg4  16054  ushgredgedg  16065  ushgredgedgloop  16067  vtxd0nedgbfi  16105  bj-inf2vnlem1  16501  bj-inf2vnlem2  16502  bj-nn0sucALT  16509  sscoll2  16519  3dom  16523  subctctexmid  16537  pw1nct  16540  isomninnlem  16570  trilpolemlt1  16581  trirec0  16584  ismkvnnlem  16592