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  11100  shftfval  11103  rexfiuz  11271  recvguniq  11277  fimaxre2  11509  clim  11563  sumeq1  11637  summodc  11665  fsum3  11669  mertenslemub  11816  mertenslemi1  11817  mertenslem2  11818  mertensabs  11819  prodeq1f  11834  prodeq2w  11838  prodmodc  11860  fprodseq  11865  divides  12071  odd2np1lem  12154  opeo  12179  omeo  12180  divalglemeunn  12203  divalglemeuneg  12205  zeqzmulgcd  12262  bezoutlemnewy  12288  bezoutlemmain  12290  bezoutlemex  12293  bezoutlemaz  12295  exprmfct  12431  nnnn0modprm0  12549  pceu  12589  pcprmpw2  12627  4sqlemafi  12689  4sqexercise1  12692  4sqlem12  12696  ennnfoneleminc  12753  ennnfonelemex  12756  ennnfonelemhom  12757  ennnfonelemnn0  12764  ennnfonelemr  12765  ctinfomlemom  12769  ctinfom  12770  nninfdclemcl  12790  nninfdclemp1  12792  nninfdc  12795  ptex  13067  grpinvalem  13188  igsumvalx  13192  gsumpropd  13195  gsumress  13198  gsum0g  13199  isnsgrp  13209  grpinvex  13313  dfgrp2  13330  grpidinv2  13361  grpidinv  13362  dfgrp3mlem  13401  grp1  13409  imasgrp2  13417  dvdsrd  13827  opprunitd  13843  subrgdvds  13968  lss1d  14116  lspsn  14149  ellspsn  14150  rspsn  14267  znf1o  14384  basis2  14491  eltg2  14496  tg2  14503  neival  14586  isnei  14587  isneip  14589  restbasg  14611  cnpval  14641  iscnp  14642  icnpimaex  14654  lmbr  14656  lmbr2  14657  cnptoprest2  14683  lmff  14692  txbas  14701  txcnp  14714  txrest  14719  blssps  14870  blss  14871  mopni  14925  metss  14937  metrest  14949  metcnp3  14954  divcnap  15008  cncfval  15015  elcncf2  15017  cncfmet  15035  dedekindeulemuub  15060  dedekindeulemloc  15062  dedekindeulemlu  15064  suplociccreex  15067  dedekindicclemuub  15069  dedekindicclemloc  15071  dedekindicclemlu  15073  ivthreinc  15088  limccl  15102  ellimc3apf  15103  limcdifap  15105  limcmpted  15106  plyval  15175  elply2  15178  2lgslem1b  15537  bj-inf2vnlem1  15868  bj-inf2vnlem2  15869  bj-nn0sucALT  15876  sscoll2  15886  subctctexmid  15899  pw1nct  15902  isomninnlem  15931  trilpolemlt1  15942  trirec0  15945  ismkvnnlem  15953