Theorem rexbidv 2533

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

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

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-rex 2516

This theorem is referenced by:  rexbii  2539  2rexbidv  2557  rexralbidv  2558  rexeqbi1dv  2743  rexeqbidv  2747  cbvrex2vw  2779  cbvrex2v  2781  rspc2ev  2925  rspc3ev  2927  ceqsrex2v  2938  sbcrext  3109  uniiunlem  3316  eliun  3974  dfiin2g  4003  dfiunv2  4006  nn0suc  4702  rexxpf  4877  elrnmpt  4981  elrnmptg  4984  elimag  5080  funcnvuni  5399  fun11iun  5604  fvelrnb  5693  fvelimab  5702  foco2  5893  elabrex  5897  elabrexg  5898  abrexco  5899  f1oiso  5966  f1oiso2  5967  acexmidlemab  6011  acexmidlemcase  6012  abrexex2g  6281  abrexex2  6285  recseq  6471  tfr0dm  6487  tfr1onlemaccex  6513  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllemaccex  6526  tfrcllemres  6527  freceq1  6557  frec0g  6562  freccllem  6567  frecfcllem  6569  frecsuclem  6571  frecsuc  6572  nnaordex  6695  qseq2  6752  elqsg  6753  elixpsn  6903  ixpsnf1o  6904  isfi  6933  enfi  7059  fimax2gtri  7090  elfi  7169  supeq3  7188  supmoti  7191  suplubti  7198  supisolem  7206  cnvinfex  7216  eqinfti  7218  infvalti  7220  infglbti  7223  enomnilem  7336  finomni  7338  exmidomni  7340  fodjum  7344  fodju0  7345  fodjuomnilemres  7346  fodjuomni  7347  ismkvnex  7353  fodjumkvlemres  7357  fodjumkv  7358  enmkvlem  7359  ltexnqq  7627  elinp  7693  prnmaxl  7707  prnminu  7708  prarloclem3  7716  ltdfpr  7725  genpdflem  7726  genipv  7728  genpassl  7743  genpassu  7744  ltexprlemm  7819  ltexprlemloc  7826  cauappcvgprlemm  7864  cauappcvgprlemopl  7865  cauappcvgprlemlol  7866  cauappcvgprlemopu  7867  cauappcvgprlemupu  7868  cauappcvgprlemdisj  7870  cauappcvgprlemloc  7871  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  cauappcvgprlem1  7878  cauappcvgprlem2  7879  caucvgprlemm  7887  caucvgprlemopl  7888  caucvgprlemlol  7889  caucvgprlemopu  7890  caucvgprlemupu  7891  caucvgprlemdisj  7893  caucvgprlemloc  7894  caucvgprlemladdfu  7896  caucvgprlemladdrl  7897  caucvgprlem1  7898  caucvgprlem2  7899  caucvgprprlemell  7904  caucvgprprlemelu  7905  caucvgprprlemml  7913  caucvgprprlemmu  7914  caucvgprprlemexbt  7925  caucvgprprlem2  7929  suplocexprlemmu  7937  suplocexprlemru  7938  suplocexprlemdisj  7939  suplocexprlemloc  7940  suplocexprlemub  7942  recexgt0sr  7992  archsr  8001  map2psrprg  8024  suplocsrlemb  8025  axprecex  8099  nntopi  8113  axpre-suploclemres  8120  axpre-suploc  8121  cnegex  8356  apreap  8766  recexap  8832  sup3exmid  9136  creur  9138  creui  9139  cju  9140  supinfneg  9828  infsupneg  9829  infssuzex  10492  nninfdcex  10496  exbtwnzlemshrink  10507  rebtwn2zlemshrink  10512  modqmuladd  10627  hashunlem  11066  iswrd  11114  csbwrdg  11142  shftfvalg  11378  shftfval  11381  rexfiuz  11549  recvguniq  11555  fimaxre2  11787  clim  11841  sumeq1  11915  summodc  11943  fsum3  11947  mertenslemub  12094  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  prodeq1f  12112  prodeq2w  12116  prodmodc  12138  fprodseq  12143  divides  12349  odd2np1lem  12432  opeo  12457  omeo  12458  divalglemeunn  12481  divalglemeuneg  12483  zeqzmulgcd  12540  bezoutlemnewy  12566  bezoutlemmain  12568  bezoutlemex  12571  bezoutlemaz  12573  exprmfct  12709  nnnn0modprm0  12827  pceu  12867  pcprmpw2  12905  4sqlemafi  12967  4sqexercise1  12970  4sqlem12  12974  ennnfoneleminc  13031  ennnfonelemex  13034  ennnfonelemhom  13035  ennnfonelemnn0  13042  ennnfonelemr  13043  ctinfomlemom  13047  ctinfom  13048  nninfdclemcl  13068  nninfdclemp1  13070  nninfdc  13073  ptex  13346  grpinvalem  13467  igsumvalx  13471  gsumpropd  13474  gsumress  13477  gsum0g  13478  isnsgrp  13488  grpinvex  13592  dfgrp2  13609  grpidinv2  13640  grpidinv  13641  dfgrp3mlem  13680  grp1  13688  imasgrp2  13696  dvdsrd  14107  opprunitd  14123  subrgdvds  14248  lss1d  14396  lspsn  14429  ellspsn  14430  rspsn  14547  znf1o  14664  basis2  14771  eltg2  14776  tg2  14783  neival  14866  isnei  14867  isneip  14869  restbasg  14891  cnpval  14921  iscnp  14922  icnpimaex  14934  lmbr  14936  lmbr2  14937  cnptoprest2  14963  lmff  14972  txbas  14981  txcnp  14994  txrest  14999  blssps  15150  blss  15151  mopni  15205  metss  15217  metrest  15229  metcnp3  15234  divcnap  15288  cncfval  15295  elcncf2  15297  cncfmet  15315  dedekindeulemuub  15340  dedekindeulemloc  15342  dedekindeulemlu  15344  suplociccreex  15347  dedekindicclemuub  15349  dedekindicclemloc  15351  dedekindicclemlu  15353  ivthreinc  15368  limccl  15382  ellimc3apf  15383  limcdifap  15385  limcmpted  15386  plyval  15455  elply2  15458  2lgslem1b  15817  upgredg2vtx  15998  usgredg4  16065  ushgredgedg  16076  ushgredgedgloop  16078  vtxd0nedgbfi  16149  bj-inf2vnlem1  16565  bj-inf2vnlem2  16566  bj-nn0sucALT  16573  sscoll2  16583  3dom  16587  subctctexmid  16601  pw1nct  16604  isomninnlem  16634  trilpolemlt1  16645  trirec0  16648  ismkvnnlem  16656