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 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105  ∃wrex 2529

This proof depends on 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 proof depends on definitions:  df-bi 117  df-nf 1514  df-rex 2534

This theorem is used 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  4016  dfiin2g  4045  dfiunv2  4048  nn0suc  4753  rexxpf  4929  elrnmpt  5033  elrnmptg  5036  elimag  5133  funcnvuni  5453  fun11iun  5663  fvelrnb  5753  fvelimab  5762  foco2  5962  elabrex  5966  elabrexg  5967  abrexco  5968  f1oiso  6035  f1oiso2  6036  acexmidlemab  6082  acexmidlemcase  6083  abrexex2g  6353  abrexex2  6357  elabreximd  6360  recseq  6581  tfr0dm  6597  tfr1onlemaccex  6623  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllemaccex  6636  tfrcllemres  6637  freceq1  6667  frec0g  6672  freccllem  6677  frecfcllem  6679  frecsuclem  6681  frecsuc  6682  nnaordex  6805  qseq2  6862  elqsg  6863  elixpsn  7021  ixpsnf1o  7022  isfi  7051  enfi  7179  fimax2gtri  7210  elfi  7310  supeq3  7336  supmoti  7339  suplubti  7346  supisolem  7354  cnvinfex  7364  eqinfti  7366  infvalti  7368  infglbti  7371  enomnilem  7484  finomni  7486  exmidomni  7488  fodjum  7492  fodju0  7493  fodjuomnilemres  7494  fodjuomni  7495  ismkvnex  7501  fodjumkvlemres  7505  fodjumkv  7506  enmkvlem  7507  ltexnqq  7781  elinp  7847  prnmaxl  7861  prnminu  7862  prarloclem3  7870  ltdfpr  7879  genpdflem  7880  genipv  7882  genpassl  7897  genpassu  7898  ltexprlemm  7973  ltexprlemloc  7980  cauappcvgprlemm  8018  cauappcvgprlemopl  8019  cauappcvgprlemlol  8020  cauappcvgprlemopu  8021  cauappcvgprlemupu  8022  cauappcvgprlemdisj  8024  cauappcvgprlemloc  8025  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  cauappcvgprlem1  8032  cauappcvgprlem2  8033  caucvgprlemm  8041  caucvgprlemopl  8042  caucvgprlemlol  8043  caucvgprlemopu  8044  caucvgprlemupu  8045  caucvgprlemdisj  8047  caucvgprlemloc  8048  caucvgprlemladdfu  8050  caucvgprlemladdrl  8051  caucvgprlem1  8052  caucvgprlem2  8053  caucvgprprlemell  8058  caucvgprprlemelu  8059  caucvgprprlemml  8067  caucvgprprlemmu  8068  caucvgprprlemexbt  8079  caucvgprprlem2  8083  suplocexprlemmu  8091  suplocexprlemru  8092  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemub  8096  recexgt0sr  8146  archsr  8155  map2psrprg  8178  suplocsrlemb  8179  axprecex  8253  nntopi  8267  axpre-suploclemres  8274  axpre-suploc  8275  cnegex  8511  apreap  8923  recexap  8989  sup3exmid  9295  creur  9297  creui  9298  cju  9299  supinfneg  10011  infsupneg  10012  infssuzex  10683  nninfdcex  10689  exbtwnzlemshrink  10700  rebtwn2zlemshrink  10705  modqmuladd  10824  hashunlem  11266  iswrd  11328  csbwrdg  11356  shftfvalg  11605  shftfval  11608  rexfiuz  11777  recvguniq  11783  fimaxre2  12016  fiidxsupcl  12018  clim  12072  sumeq1  12146  summodc  12175  fsum3  12179  mertenslemub  12326  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  prodeq1f  12344  prodeq2w  12348  prodmodc  12370  fprodseq  12375  divides  12581  odd2np1lem  12664  opeo  12689  omeo  12690  divalglemeunn  12713  divalglemeuneg  12715  zeqzmulgcd  12772  bezoutlemnewy  12798  bezoutlemmain  12800  bezoutlemex  12803  bezoutlemaz  12805  exprmfct  12942  nnnn0modprm0  13063  pceu  13103  pcprmpw2  13141  4sqlemafi  13203  4sqexercise1  13206  4sqlem12  13210  ennnfoneleminc  13360  ennnfonelemex  13363  ennnfonelemhom  13364  ennnfonelemnn0  13371  ennnfonelemr  13372  ctinfomlemom  13376  ctinfom  13377  nninfdclemcl  13397  nninfdclemp1  13399  nninfdc  13402  ptex  13677  grpinvalem  13764  gzsumvalx  13768  gzsumress  13771  gzsum0  13772  isnsgrp  13780  grpinvex  13874  dfgrp2  13891  grpidinv2  13922  grpidinv  13923  dfgrp3mlem  13962  grp1  13970  imasgrp2  13972  dvdsrd  14510  opprunitd  14526  subrgdvds  14652  lss1d  14829  lspsn  14862  ellspsn  14863  rspsn  14980  znf1o  15095  basis2  15274  eltg2  15279  tg2  15286  neival  15369  isnei  15370  isneip  15372  restbasg  15394  cnpval  15424  iscnp  15425  icnpimaex  15437  lmbr  15439  lmbr2  15440  cnptoprest2  15466  lmff  15475  txbas  15484  txcnp  15497  txrest  15502  blssps  15653  blss  15654  mopni  15708  metss  15720  metrest  15732  metcnp3  15737  divcnap  15791  cncfval  15798  elcncf2  15800  cncfmet  15818  dedekindeulemuub  15843  dedekindeulemloc  15845  dedekindeulemlu  15847  suplociccreex  15850  dedekindicclemuub  15852  dedekindicclemloc  15854  dedekindicclemlu  15856  ivthreinc  15871  limccl  15885  ellimc3apf  15886  limcdifap  15888  limcmpted  15889  plyval  15958  elply2  15961  2lgslem1b  16413  upgredg2vtx  16594  usgredg4  16661  ushgredgedg  16672  ushgredgedgloop  16674  vtxd0nedgbfi  16745  bj-inf2vnlem1  17201  bj-inf2vnlem2  17202  bj-nn0sucALT  17209  sscoll2  17219  3dom  17223  subctctexmid  17235  pw1nct  17238  isomninnlem  17285  trilpolemlt1  17297  trirec0  17300  qdiff  17305  ismkvnnlem  17309