Theorem rexbidv 2551

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

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

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-rex 2534

This theorem is referenced by:  rexbii  2557  2rexbidv  2575  rexralbidv  2576  rexeqbi1dv  2762  rexeqbidv  2766  cbvrex2vw  2798  cbvrex2v  2800  rspc2ev  2945  rspc3ev  2947  ceqsrex2v  2958  sbcrext  3129  uniiunlem  3338  eliun  4011  dfiin2g  4040  dfiunv2  4043  nn0suc  4746  rexxpf  4922  elrnmpt  5026  elrnmptg  5029  elimag  5125  funcnvuni  5445  fun11iun  5655  fvelrnb  5744  fvelimab  5753  foco2  5949  elabrex  5953  elabrexg  5954  abrexco  5955  f1oiso  6022  f1oiso2  6023  acexmidlemab  6069  acexmidlemcase  6070  abrexex2g  6339  abrexex2  6343  elabreximd  6346  recseq  6567  tfr0dm  6583  tfr1onlemaccex  6609  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  tfrcllemaccex  6622  tfrcllemres  6623  freceq1  6653  frec0g  6658  freccllem  6663  frecfcllem  6665  frecsuclem  6667  frecsuc  6668  nnaordex  6791  qseq2  6848  elqsg  6849  elixpsn  7007  ixpsnf1o  7008  isfi  7037  enfi  7165  fimax2gtri  7196  elfi  7295  supeq3  7320  supmoti  7323  suplubti  7330  supisolem  7338  cnvinfex  7348  eqinfti  7350  infvalti  7352  infglbti  7355  enomnilem  7468  finomni  7470  exmidomni  7472  fodjum  7476  fodju0  7477  fodjuomnilemres  7478  fodjuomni  7479  ismkvnex  7485  fodjumkvlemres  7489  fodjumkv  7490  enmkvlem  7491  ltexnqq  7765  elinp  7831  prnmaxl  7845  prnminu  7846  prarloclem3  7854  ltdfpr  7863  genpdflem  7864  genipv  7866  genpassl  7881  genpassu  7882  ltexprlemm  7957  ltexprlemloc  7964  cauappcvgprlemm  8002  cauappcvgprlemopl  8003  cauappcvgprlemlol  8004  cauappcvgprlemopu  8005  cauappcvgprlemupu  8006  cauappcvgprlemdisj  8008  cauappcvgprlemloc  8009  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  cauappcvgprlem1  8016  cauappcvgprlem2  8017  caucvgprlemm  8025  caucvgprlemopl  8026  caucvgprlemlol  8027  caucvgprlemopu  8028  caucvgprlemupu  8029  caucvgprlemdisj  8031  caucvgprlemloc  8032  caucvgprlemladdfu  8034  caucvgprlemladdrl  8035  caucvgprlem1  8036  caucvgprlem2  8037  caucvgprprlemell  8042  caucvgprprlemelu  8043  caucvgprprlemml  8051  caucvgprprlemmu  8052  caucvgprprlemexbt  8063  caucvgprprlem2  8067  suplocexprlemmu  8075  suplocexprlemru  8076  suplocexprlemdisj  8077  suplocexprlemloc  8078  suplocexprlemub  8080  recexgt0sr  8130  archsr  8139  map2psrprg  8162  suplocsrlemb  8163  axprecex  8237  nntopi  8251  axpre-suploclemres  8258  axpre-suploc  8259  cnegex  8494  apreap  8905  recexap  8971  sup3exmid  9277  creur  9279  creui  9280  cju  9281  supinfneg  9974  infsupneg  9975  infssuzex  10644  nninfdcex  10650  exbtwnzlemshrink  10661  rebtwn2zlemshrink  10666  modqmuladd  10781  hashunlem  11222  iswrd  11284  csbwrdg  11312  shftfvalg  11561  shftfval  11564  rexfiuz  11733  recvguniq  11739  fimaxre2  11971  clim  12025  sumeq1  12099  summodc  12128  fsum3  12132  mertenslemub  12279  mertenslemi1  12280  mertenslem2  12281  mertensabs  12282  prodeq1f  12297  prodeq2w  12301  prodmodc  12323  fprodseq  12328  divides  12534  odd2np1lem  12617  opeo  12642  omeo  12643  divalglemeunn  12666  divalglemeuneg  12668  zeqzmulgcd  12725  bezoutlemnewy  12751  bezoutlemmain  12753  bezoutlemex  12756  bezoutlemaz  12758  exprmfct  12894  nnnn0modprm0  13012  pceu  13052  pcprmpw2  13090  4sqlemafi  13152  4sqexercise1  13155  4sqlem12  13159  ennnfoneleminc  13280  ennnfonelemex  13283  ennnfonelemhom  13284  ennnfonelemnn0  13291  ennnfonelemr  13292  ctinfomlemom  13296  ctinfom  13297  nninfdclemcl  13317  nninfdclemp1  13319  nninfdc  13322  ptex  13595  grpinvalem  13682  gzsumvalx  13686  gzsumress  13689  gzsum0  13690  isnsgrp  13698  grpinvex  13792  dfgrp2  13809  grpidinv2  13840  grpidinv  13841  dfgrp3mlem  13880  grp1  13888  imasgrp2  13890  dvdsrd  14374  opprunitd  14390  subrgdvds  14516  lss1d  14692  lspsn  14725  ellspsn  14726  rspsn  14843  znf1o  14958  basis2  15072  eltg2  15077  tg2  15084  neival  15167  isnei  15168  isneip  15170  restbasg  15192  cnpval  15222  iscnp  15223  icnpimaex  15235  lmbr  15237  lmbr2  15238  cnptoprest2  15264  lmff  15273  txbas  15282  txcnp  15295  txrest  15300  blssps  15451  blss  15452  mopni  15506  metss  15518  metrest  15530  metcnp3  15535  divcnap  15589  cncfval  15596  elcncf2  15598  cncfmet  15616  dedekindeulemuub  15641  dedekindeulemloc  15643  dedekindeulemlu  15645  suplociccreex  15648  dedekindicclemuub  15650  dedekindicclemloc  15652  dedekindicclemlu  15654  ivthreinc  15669  limccl  15683  ellimc3apf  15684  limcdifap  15686  limcmpted  15687  plyval  15756  elply2  15759  2lgslem1b  16122  upgredg2vtx  16303  usgredg4  16370  ushgredgedg  16381  ushgredgedgloop  16383  vtxd0nedgbfi  16454  bj-inf2vnlem1  16910  bj-inf2vnlem2  16911  bj-nn0sucALT  16918  sscoll2  16928  3dom  16932  subctctexmid  16944  pw1nct  16947  isomninnlem  16984  trilpolemlt1  16995  trirec0  16998  qdiff  17003  ismkvnnlem  17007