Theorem rexbidv 2490

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

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

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-rex 2473

This theorem is referenced by:  rexbii  2496  2rexbidv  2514  rexralbidv  2515  rexeqbi1dv  2694  rexeqbidv  2698  cbvrex2vw  2729  cbvrex2v  2731  rspc2ev  2870  rspc3ev  2872  ceqsrex2v  2883  sbcrext  3054  uniiunlem  3258  eliun  3904  dfiin2g  3933  dfiunv2  3936  nn0suc  4617  rexxpf  4788  elrnmpt  4890  elrnmptg  4893  elimag  4988  funcnvuni  5299  fun11iun  5496  fvelrnb  5578  fvelimab  5587  foco2  5769  elabrex  5773  elabrexg  5774  abrexco  5775  f1oiso  5842  f1oiso2  5843  acexmidlemab  5884  acexmidlemcase  5885  abrexex2g  6138  abrexex2  6142  recseq  6324  tfr0dm  6340  tfr1onlemaccex  6366  tfrcllemsucaccv  6372  tfrcllembxssdm  6374  tfrcllemaccex  6379  tfrcllemres  6380  freceq1  6410  frec0g  6415  freccllem  6420  frecfcllem  6422  frecsuclem  6424  frecsuc  6425  nnaordex  6546  qseq2  6601  elqsg  6602  elixpsn  6752  ixpsnf1o  6753  isfi  6778  enfi  6890  fimax2gtri  6918  elfi  6987  supeq3  7006  supmoti  7009  suplubti  7016  supisolem  7024  cnvinfex  7034  eqinfti  7036  infvalti  7038  infglbti  7041  enomnilem  7153  finomni  7155  exmidomni  7157  fodjum  7161  fodju0  7162  fodjuomnilemres  7163  fodjuomni  7164  ismkvnex  7170  fodjumkvlemres  7174  fodjumkv  7175  enmkvlem  7176  ltexnqq  7424  elinp  7490  prnmaxl  7504  prnminu  7505  prarloclem3  7513  ltdfpr  7522  genpdflem  7523  genipv  7525  genpassl  7540  genpassu  7541  ltexprlemm  7616  ltexprlemloc  7623  cauappcvgprlemm  7661  cauappcvgprlemopl  7662  cauappcvgprlemlol  7663  cauappcvgprlemopu  7664  cauappcvgprlemupu  7665  cauappcvgprlemdisj  7667  cauappcvgprlemloc  7668  cauappcvgprlemladdfu  7670  cauappcvgprlemladdfl  7671  cauappcvgprlemladdru  7672  cauappcvgprlemladdrl  7673  cauappcvgprlem1  7675  cauappcvgprlem2  7676  caucvgprlemm  7684  caucvgprlemopl  7685  caucvgprlemlol  7686  caucvgprlemopu  7687  caucvgprlemupu  7688  caucvgprlemdisj  7690  caucvgprlemloc  7691  caucvgprlemladdfu  7693  caucvgprlemladdrl  7694  caucvgprlem1  7695  caucvgprlem2  7696  caucvgprprlemell  7701  caucvgprprlemelu  7702  caucvgprprlemml  7710  caucvgprprlemmu  7711  caucvgprprlemexbt  7722  caucvgprprlem2  7726  suplocexprlemmu  7734  suplocexprlemru  7735  suplocexprlemdisj  7736  suplocexprlemloc  7737  suplocexprlemub  7739  recexgt0sr  7789  archsr  7798  map2psrprg  7821  suplocsrlemb  7822  axprecex  7896  nntopi  7910  axpre-suploclemres  7917  axpre-suploc  7918  cnegex  8152  apreap  8561  recexap  8627  sup3exmid  8931  creur  8933  creui  8934  cju  8935  supinfneg  9612  infsupneg  9613  exbtwnzlemshrink  10266  rebtwn2zlemshrink  10271  modqmuladd  10383  hashunlem  10801  shftfvalg  10844  shftfval  10847  rexfiuz  11015  recvguniq  11021  fimaxre2  11252  clim  11306  sumeq1  11380  summodc  11408  fsum3  11412  mertenslemub  11559  mertenslemi1  11560  mertenslem2  11561  mertensabs  11562  prodeq1f  11577  prodeq2w  11581  prodmodc  11603  fprodseq  11608  divides  11813  odd2np1lem  11894  opeo  11919  omeo  11920  divalglemeunn  11943  divalglemeuneg  11945  infssuzex  11967  nninfdcex  11971  zeqzmulgcd  11988  bezoutlemnewy  12014  bezoutlemmain  12016  bezoutlemex  12019  bezoutlemaz  12021  exprmfct  12155  nnnn0modprm0  12272  pceu  12312  pcprmpw2  12349  ennnfoneleminc  12429  ennnfonelemex  12432  ennnfonelemhom  12433  ennnfonelemnn0  12440  ennnfonelemr  12441  ctinfomlemom  12445  ctinfom  12446  nninfdclemcl  12466  nninfdclemp1  12468  nninfdc  12471  ptex  12734  grpinvalem  12826  isnsgrp  12834  grpinvex  12920  dfgrp2  12936  grpidinv2  12967  grpidinv  12968  dfgrp3mlem  13007  grp1  13015  imasgrp2  13017  dvdsrd  13404  opprunitd  13420  subrgdvds  13542  lss1d  13659  lspsn  13692  lspsnel  13693  basis2  13931  eltg2  13936  tg2  13943  neival  14026  isnei  14027  isneip  14029  restbasg  14051  cnpval  14081  iscnp  14082  icnpimaex  14094  lmbr  14096  lmbr2  14097  cnptoprest2  14123  lmff  14132  txbas  14141  txcnp  14154  txrest  14159  blssps  14310  blss  14311  mopni  14365  metss  14377  metrest  14389  metcnp3  14394  divcnap  14438  cncfval  14442  elcncf2  14444  cncfmet  14462  dedekindeulemuub  14478  dedekindeulemloc  14480  dedekindeulemlu  14482  suplociccreex  14485  dedekindicclemuub  14487  dedekindicclemloc  14489  dedekindicclemlu  14491  limccl  14511  ellimc3apf  14512  limcdifap  14514  limcmpted  14515  bj-inf2vnlem1  15105  bj-inf2vnlem2  15106  bj-nn0sucALT  15113  sscoll2  15123  subctctexmid  15134  pw1nct  15136  isomninnlem  15162  trilpolemlt1  15173  trirec0  15176  ismkvnnlem  15184