Theorem rexbidv 2531

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

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

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-rex 2514

This theorem is referenced by:  rexbii  2537  2rexbidv  2555  rexralbidv  2556  rexeqbi1dv  2741  rexeqbidv  2745  cbvrex2vw  2777  cbvrex2v  2779  rspc2ev  2922  rspc3ev  2924  ceqsrex2v  2935  sbcrext  3106  uniiunlem  3313  eliun  3969  dfiin2g  3998  dfiunv2  4001  nn0suc  4696  rexxpf  4869  elrnmpt  4973  elrnmptg  4976  elimag  5072  funcnvuni  5390  fun11iun  5595  fvelrnb  5683  fvelimab  5692  foco2  5883  elabrex  5887  elabrexg  5888  abrexco  5889  f1oiso  5956  f1oiso2  5957  acexmidlemab  6001  acexmidlemcase  6002  abrexex2g  6271  abrexex2  6275  recseq  6458  tfr0dm  6474  tfr1onlemaccex  6500  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllemaccex  6513  tfrcllemres  6514  freceq1  6544  frec0g  6549  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecsuc  6559  nnaordex  6682  qseq2  6739  elqsg  6740  elixpsn  6890  ixpsnf1o  6891  isfi  6920  enfi  7043  fimax2gtri  7072  elfi  7149  supeq3  7168  supmoti  7171  suplubti  7178  supisolem  7186  cnvinfex  7196  eqinfti  7198  infvalti  7200  infglbti  7203  enomnilem  7316  finomni  7318  exmidomni  7320  fodjum  7324  fodju0  7325  fodjuomnilemres  7326  fodjuomni  7327  ismkvnex  7333  fodjumkvlemres  7337  fodjumkv  7338  enmkvlem  7339  ltexnqq  7606  elinp  7672  prnmaxl  7686  prnminu  7687  prarloclem3  7695  ltdfpr  7704  genpdflem  7705  genipv  7707  genpassl  7722  genpassu  7723  ltexprlemm  7798  ltexprlemloc  7805  cauappcvgprlemm  7843  cauappcvgprlemopl  7844  cauappcvgprlemlol  7845  cauappcvgprlemopu  7846  cauappcvgprlemupu  7847  cauappcvgprlemdisj  7849  cauappcvgprlemloc  7850  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem1  7857  cauappcvgprlem2  7858  caucvgprlemm  7866  caucvgprlemopl  7867  caucvgprlemlol  7868  caucvgprlemopu  7869  caucvgprlemupu  7870  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  caucvgprlem1  7877  caucvgprlem2  7878  caucvgprprlemell  7883  caucvgprprlemelu  7884  caucvgprprlemml  7892  caucvgprprlemmu  7893  caucvgprprlemexbt  7904  caucvgprprlem2  7908  suplocexprlemmu  7916  suplocexprlemru  7917  suplocexprlemdisj  7918  suplocexprlemloc  7919  suplocexprlemub  7921  recexgt0sr  7971  archsr  7980  map2psrprg  8003  suplocsrlemb  8004  axprecex  8078  nntopi  8092  axpre-suploclemres  8099  axpre-suploc  8100  cnegex  8335  apreap  8745  recexap  8811  sup3exmid  9115  creur  9117  creui  9118  cju  9119  supinfneg  9802  infsupneg  9803  infssuzex  10465  nninfdcex  10469  exbtwnzlemshrink  10480  rebtwn2zlemshrink  10485  modqmuladd  10600  hashunlem  11038  iswrd  11086  csbwrdg  11114  shftfvalg  11344  shftfval  11347  rexfiuz  11515  recvguniq  11521  fimaxre2  11753  clim  11807  sumeq1  11881  summodc  11909  fsum3  11913  mertenslemub  12060  mertenslemi1  12061  mertenslem2  12062  mertensabs  12063  prodeq1f  12078  prodeq2w  12082  prodmodc  12104  fprodseq  12109  divides  12315  odd2np1lem  12398  opeo  12423  omeo  12424  divalglemeunn  12447  divalglemeuneg  12449  zeqzmulgcd  12506  bezoutlemnewy  12532  bezoutlemmain  12534  bezoutlemex  12537  bezoutlemaz  12539  exprmfct  12675  nnnn0modprm0  12793  pceu  12833  pcprmpw2  12871  4sqlemafi  12933  4sqexercise1  12936  4sqlem12  12940  ennnfoneleminc  12997  ennnfonelemex  13000  ennnfonelemhom  13001  ennnfonelemnn0  13008  ennnfonelemr  13009  ctinfomlemom  13013  ctinfom  13014  nninfdclemcl  13034  nninfdclemp1  13036  nninfdc  13039  ptex  13312  grpinvalem  13433  igsumvalx  13437  gsumpropd  13440  gsumress  13443  gsum0g  13444  isnsgrp  13454  grpinvex  13558  dfgrp2  13575  grpidinv2  13606  grpidinv  13607  dfgrp3mlem  13646  grp1  13654  imasgrp2  13662  dvdsrd  14073  opprunitd  14089  subrgdvds  14214  lss1d  14362  lspsn  14395  ellspsn  14396  rspsn  14513  znf1o  14630  basis2  14737  eltg2  14742  tg2  14749  neival  14832  isnei  14833  isneip  14835  restbasg  14857  cnpval  14887  iscnp  14888  icnpimaex  14900  lmbr  14902  lmbr2  14903  cnptoprest2  14929  lmff  14938  txbas  14947  txcnp  14960  txrest  14965  blssps  15116  blss  15117  mopni  15171  metss  15183  metrest  15195  metcnp3  15200  divcnap  15254  cncfval  15261  elcncf2  15263  cncfmet  15281  dedekindeulemuub  15306  dedekindeulemloc  15308  dedekindeulemlu  15310  suplociccreex  15313  dedekindicclemuub  15315  dedekindicclemloc  15317  dedekindicclemlu  15319  ivthreinc  15334  limccl  15348  ellimc3apf  15349  limcdifap  15351  limcmpted  15352  plyval  15421  elply2  15424  2lgslem1b  15783  upgredg2vtx  15961  usgredg4  16028  ushgredgedg  16039  ushgredgedgloop  16041  bj-inf2vnlem1  16388  bj-inf2vnlem2  16389  bj-nn0sucALT  16396  sscoll2  16406  3dom  16411  subctctexmid  16425  pw1nct  16428  isomninnlem  16458  trilpolemlt1  16469  trirec0  16472  ismkvnnlem  16480