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  5894  elabrex  5898  elabrexg  5899  abrexco  5900  f1oiso  5967  f1oiso2  5968  acexmidlemab  6012  acexmidlemcase  6013  abrexex2g  6282  abrexex2  6286  recseq  6472  tfr0dm  6488  tfr1onlemaccex  6514  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllemaccex  6527  tfrcllemres  6528  freceq1  6558  frec0g  6563  freccllem  6568  frecfcllem  6570  frecsuclem  6572  frecsuc  6573  nnaordex  6696  qseq2  6753  elqsg  6754  elixpsn  6904  ixpsnf1o  6905  isfi  6934  enfi  7060  fimax2gtri  7091  elfi  7170  supeq3  7189  supmoti  7192  suplubti  7199  supisolem  7207  cnvinfex  7217  eqinfti  7219  infvalti  7221  infglbti  7224  enomnilem  7337  finomni  7339  exmidomni  7341  fodjum  7345  fodju0  7346  fodjuomnilemres  7347  fodjuomni  7348  ismkvnex  7354  fodjumkvlemres  7358  fodjumkv  7359  enmkvlem  7360  ltexnqq  7628  elinp  7694  prnmaxl  7708  prnminu  7709  prarloclem3  7717  ltdfpr  7726  genpdflem  7727  genipv  7729  genpassl  7744  genpassu  7745  ltexprlemm  7820  ltexprlemloc  7827  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemopu  7868  cauappcvgprlemupu  7869  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  cauappcvgprlem2  7880  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemopu  7891  caucvgprlemupu  7892  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgprlem1  7899  caucvgprlem2  7900  caucvgprprlemell  7905  caucvgprprlemelu  7906  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemexbt  7926  caucvgprprlem2  7930  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemub  7943  recexgt0sr  7993  archsr  8002  map2psrprg  8025  suplocsrlemb  8026  axprecex  8100  nntopi  8114  axpre-suploclemres  8121  axpre-suploc  8122  cnegex  8357  apreap  8767  recexap  8833  sup3exmid  9137  creur  9139  creui  9140  cju  9141  supinfneg  9829  infsupneg  9830  infssuzex  10494  nninfdcex  10498  exbtwnzlemshrink  10509  rebtwn2zlemshrink  10514  modqmuladd  10629  hashunlem  11068  iswrd  11119  csbwrdg  11147  shftfvalg  11383  shftfval  11386  rexfiuz  11554  recvguniq  11560  fimaxre2  11792  clim  11846  sumeq1  11920  summodc  11949  fsum3  11953  mertenslemub  12100  mertenslemi1  12101  mertenslem2  12102  mertensabs  12103  prodeq1f  12118  prodeq2w  12122  prodmodc  12144  fprodseq  12149  divides  12355  odd2np1lem  12438  opeo  12463  omeo  12464  divalglemeunn  12487  divalglemeuneg  12489  zeqzmulgcd  12546  bezoutlemnewy  12572  bezoutlemmain  12574  bezoutlemex  12577  bezoutlemaz  12579  exprmfct  12715  nnnn0modprm0  12833  pceu  12873  pcprmpw2  12911  4sqlemafi  12973  4sqexercise1  12976  4sqlem12  12980  ennnfoneleminc  13037  ennnfonelemex  13040  ennnfonelemhom  13041  ennnfonelemnn0  13048  ennnfonelemr  13049  ctinfomlemom  13053  ctinfom  13054  nninfdclemcl  13074  nninfdclemp1  13076  nninfdc  13079  ptex  13352  grpinvalem  13473  igsumvalx  13477  gsumpropd  13480  gsumress  13483  gsum0g  13484  isnsgrp  13494  grpinvex  13598  dfgrp2  13615  grpidinv2  13646  grpidinv  13647  dfgrp3mlem  13686  grp1  13694  imasgrp2  13702  dvdsrd  14114  opprunitd  14130  subrgdvds  14255  lss1d  14403  lspsn  14436  ellspsn  14437  rspsn  14554  znf1o  14671  basis2  14778  eltg2  14783  tg2  14790  neival  14873  isnei  14874  isneip  14876  restbasg  14898  cnpval  14928  iscnp  14929  icnpimaex  14941  lmbr  14943  lmbr2  14944  cnptoprest2  14970  lmff  14979  txbas  14988  txcnp  15001  txrest  15006  blssps  15157  blss  15158  mopni  15212  metss  15224  metrest  15236  metcnp3  15241  divcnap  15295  cncfval  15302  elcncf2  15304  cncfmet  15322  dedekindeulemuub  15347  dedekindeulemloc  15349  dedekindeulemlu  15351  suplociccreex  15354  dedekindicclemuub  15356  dedekindicclemloc  15358  dedekindicclemlu  15360  ivthreinc  15375  limccl  15389  ellimc3apf  15390  limcdifap  15392  limcmpted  15393  plyval  15462  elply2  15465  2lgslem1b  15824  upgredg2vtx  16005  usgredg4  16072  ushgredgedg  16083  ushgredgedgloop  16085  vtxd0nedgbfi  16156  bj-inf2vnlem1  16591  bj-inf2vnlem2  16592  bj-nn0sucALT  16599  sscoll2  16609  3dom  16613  subctctexmid  16627  pw1nct  16630  isomninnlem  16660  trilpolemlt1  16671  trirec0  16674  qdiff  16679  ismkvnnlem  16683