Theorem rexbidv 2466

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

Syntax hints:   → wi 4   ↔ wb 104  ∃wrex 2444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-rex 2449

This theorem is referenced by:  rexbii  2472  2rexbidv  2490  rexralbidv  2491  rexeqbi1dv  2669  rexeqbidv  2673  cbvrex2vw  2703  cbvrex2v  2705  rspc2ev  2844  rspc3ev  2846  ceqsrex2v  2857  sbcrext  3027  uniiunlem  3230  eliun  3869  dfiin2g  3898  dfiunv2  3901  nn0suc  4580  rexxpf  4750  elrnmpt  4852  elrnmptg  4855  elimag  4949  funcnvuni  5256  fun11iun  5452  fvelrnb  5533  fvelimab  5541  foco2  5721  elabrex  5725  abrexco  5726  f1oiso  5793  f1oiso2  5794  acexmidlemab  5835  acexmidlemcase  5836  grprinvlem  6032  abrexex2g  6085  abrexex2  6089  recseq  6270  tfr0dm  6286  tfr1onlemaccex  6312  tfrcllemsucaccv  6318  tfrcllembxssdm  6320  tfrcllemaccex  6325  tfrcllemres  6326  freceq1  6356  frec0g  6361  freccllem  6366  frecfcllem  6368  frecsuclem  6370  frecsuc  6371  nnaordex  6491  qseq2  6546  elqsg  6547  elixpsn  6697  ixpsnf1o  6698  isfi  6723  enfi  6835  fimax2gtri  6863  elfi  6932  supeq3  6951  supmoti  6954  suplubti  6961  supisolem  6969  cnvinfex  6979  eqinfti  6981  infvalti  6983  infglbti  6986  enomnilem  7098  finomni  7100  exmidomni  7102  fodjum  7106  fodju0  7107  fodjuomnilemres  7108  fodjuomni  7109  ismkvnex  7115  fodjumkvlemres  7119  fodjumkv  7120  enmkvlem  7121  ltexnqq  7345  elinp  7411  prnmaxl  7425  prnminu  7426  prarloclem3  7434  ltdfpr  7443  genpdflem  7444  genipv  7446  genpassl  7461  genpassu  7462  ltexprlemm  7537  ltexprlemloc  7544  cauappcvgprlemm  7582  cauappcvgprlemopl  7583  cauappcvgprlemlol  7584  cauappcvgprlemopu  7585  cauappcvgprlemupu  7586  cauappcvgprlemdisj  7588  cauappcvgprlemloc  7589  cauappcvgprlemladdfu  7591  cauappcvgprlemladdfl  7592  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  cauappcvgprlem1  7596  cauappcvgprlem2  7597  caucvgprlemm  7605  caucvgprlemopl  7606  caucvgprlemlol  7607  caucvgprlemopu  7608  caucvgprlemupu  7609  caucvgprlemdisj  7611  caucvgprlemloc  7612  caucvgprlemladdfu  7614  caucvgprlemladdrl  7615  caucvgprlem1  7616  caucvgprlem2  7617  caucvgprprlemell  7622  caucvgprprlemelu  7623  caucvgprprlemml  7631  caucvgprprlemmu  7632  caucvgprprlemexbt  7643  caucvgprprlem2  7647  suplocexprlemmu  7655  suplocexprlemru  7656  suplocexprlemdisj  7657  suplocexprlemloc  7658  suplocexprlemub  7660  recexgt0sr  7710  archsr  7719  map2psrprg  7742  suplocsrlemb  7743  axprecex  7817  nntopi  7831  axpre-suploclemres  7838  axpre-suploc  7839  cnegex  8072  apreap  8481  recexap  8546  sup3exmid  8848  creur  8850  creui  8851  cju  8852  supinfneg  9529  infsupneg  9530  exbtwnzlemshrink  10180  rebtwn2zlemshrink  10185  modqmuladd  10297  hashunlem  10713  shftfvalg  10756  shftfval  10759  rexfiuz  10927  recvguniq  10933  fimaxre2  11164  clim  11218  sumeq1  11292  summodc  11320  fsum3  11324  mertenslemub  11471  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  prodeq1f  11489  prodeq2w  11493  prodmodc  11515  fprodseq  11520  divides  11725  odd2np1lem  11805  opeo  11830  omeo  11831  divalglemeunn  11854  divalglemeuneg  11856  infssuzex  11878  nninfdcex  11882  zeqzmulgcd  11899  bezoutlemnewy  11925  bezoutlemmain  11927  bezoutlemex  11930  bezoutlemaz  11932  exprmfct  12066  nnnn0modprm0  12183  pceu  12223  pcprmpw2  12260  ennnfoneleminc  12340  ennnfonelemex  12343  ennnfonelemhom  12344  ennnfonelemnn0  12351  ennnfonelemr  12352  ctinfomlemom  12356  ctinfom  12357  nninfdclemcl  12377  nninfdclemp1  12379  nninfdc  12382  basis2  12646  eltg2  12653  tg2  12660  neival  12743  isnei  12744  isneip  12746  restbasg  12768  cnpval  12798  iscnp  12799  icnpimaex  12811  lmbr  12813  lmbr2  12814  cnptoprest2  12840  lmff  12849  txbas  12858  txcnp  12871  txrest  12876  blssps  13027  blss  13028  mopni  13082  metss  13094  metrest  13106  metcnp3  13111  divcnap  13155  cncfval  13159  elcncf2  13161  cncfmet  13179  dedekindeulemuub  13195  dedekindeulemloc  13197  dedekindeulemlu  13199  suplociccreex  13202  dedekindicclemuub  13204  dedekindicclemloc  13206  dedekindicclemlu  13208  limccl  13228  ellimc3apf  13229  limcdifap  13231  limcmpted  13232  bj-inf2vnlem1  13812  bj-inf2vnlem2  13813  bj-nn0sucALT  13820  sscoll2  13830  subctctexmid  13841  pw1nct  13843  isomninnlem  13869  trilpolemlt1  13880  trirec0  13883  ismkvnnlem  13891