Theorem rexbidv 2508

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

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

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-rex 2491

This theorem is referenced by:  rexbii  2514  2rexbidv  2532  rexralbidv  2533  rexeqbi1dv  2716  rexeqbidv  2720  cbvrex2vw  2751  cbvrex2v  2753  rspc2ev  2896  rspc3ev  2898  ceqsrex2v  2909  sbcrext  3080  uniiunlem  3286  eliun  3937  dfiin2g  3966  dfiunv2  3969  nn0suc  4660  rexxpf  4833  elrnmpt  4936  elrnmptg  4939  elimag  5035  funcnvuni  5352  fun11iun  5555  fvelrnb  5639  fvelimab  5648  foco2  5835  elabrex  5839  elabrexg  5840  abrexco  5841  f1oiso  5908  f1oiso2  5909  acexmidlemab  5951  acexmidlemcase  5952  abrexex2g  6218  abrexex2  6222  recseq  6405  tfr0dm  6421  tfr1onlemaccex  6447  tfrcllemsucaccv  6453  tfrcllembxssdm  6455  tfrcllemaccex  6460  tfrcllemres  6461  freceq1  6491  frec0g  6496  freccllem  6501  frecfcllem  6503  frecsuclem  6505  frecsuc  6506  nnaordex  6627  qseq2  6684  elqsg  6685  elixpsn  6835  ixpsnf1o  6836  isfi  6865  enfi  6985  fimax2gtri  7013  elfi  7088  supeq3  7107  supmoti  7110  suplubti  7117  supisolem  7125  cnvinfex  7135  eqinfti  7137  infvalti  7139  infglbti  7142  enomnilem  7255  finomni  7257  exmidomni  7259  fodjum  7263  fodju0  7264  fodjuomnilemres  7265  fodjuomni  7266  ismkvnex  7272  fodjumkvlemres  7276  fodjumkv  7277  enmkvlem  7278  ltexnqq  7541  elinp  7607  prnmaxl  7621  prnminu  7622  prarloclem3  7630  ltdfpr  7639  genpdflem  7640  genipv  7642  genpassl  7657  genpassu  7658  ltexprlemm  7733  ltexprlemloc  7740  cauappcvgprlemm  7778  cauappcvgprlemopl  7779  cauappcvgprlemlol  7780  cauappcvgprlemopu  7781  cauappcvgprlemupu  7782  cauappcvgprlemdisj  7784  cauappcvgprlemloc  7785  cauappcvgprlemladdfu  7787  cauappcvgprlemladdfl  7788  cauappcvgprlemladdru  7789  cauappcvgprlemladdrl  7790  cauappcvgprlem1  7792  cauappcvgprlem2  7793  caucvgprlemm  7801  caucvgprlemopl  7802  caucvgprlemlol  7803  caucvgprlemopu  7804  caucvgprlemupu  7805  caucvgprlemdisj  7807  caucvgprlemloc  7808  caucvgprlemladdfu  7810  caucvgprlemladdrl  7811  caucvgprlem1  7812  caucvgprlem2  7813  caucvgprprlemell  7818  caucvgprprlemelu  7819  caucvgprprlemml  7827  caucvgprprlemmu  7828  caucvgprprlemexbt  7839  caucvgprprlem2  7843  suplocexprlemmu  7851  suplocexprlemru  7852  suplocexprlemdisj  7853  suplocexprlemloc  7854  suplocexprlemub  7856  recexgt0sr  7906  archsr  7915  map2psrprg  7938  suplocsrlemb  7939  axprecex  8013  nntopi  8027  axpre-suploclemres  8034  axpre-suploc  8035  cnegex  8270  apreap  8680  recexap  8746  sup3exmid  9050  creur  9052  creui  9053  cju  9054  supinfneg  9736  infsupneg  9737  infssuzex  10398  nninfdcex  10402  exbtwnzlemshrink  10413  rebtwn2zlemshrink  10418  modqmuladd  10533  hashunlem  10971  iswrd  11018  csbwrdg  11045  shftfvalg  11204  shftfval  11207  rexfiuz  11375  recvguniq  11381  fimaxre2  11613  clim  11667  sumeq1  11741  summodc  11769  fsum3  11773  mertenslemub  11920  mertenslemi1  11921  mertenslem2  11922  mertensabs  11923  prodeq1f  11938  prodeq2w  11942  prodmodc  11964  fprodseq  11969  divides  12175  odd2np1lem  12258  opeo  12283  omeo  12284  divalglemeunn  12307  divalglemeuneg  12309  zeqzmulgcd  12366  bezoutlemnewy  12392  bezoutlemmain  12394  bezoutlemex  12397  bezoutlemaz  12399  exprmfct  12535  nnnn0modprm0  12653  pceu  12693  pcprmpw2  12731  4sqlemafi  12793  4sqexercise1  12796  4sqlem12  12800  ennnfoneleminc  12857  ennnfonelemex  12860  ennnfonelemhom  12861  ennnfonelemnn0  12868  ennnfonelemr  12869  ctinfomlemom  12873  ctinfom  12874  nninfdclemcl  12894  nninfdclemp1  12896  nninfdc  12899  ptex  13171  grpinvalem  13292  igsumvalx  13296  gsumpropd  13299  gsumress  13302  gsum0g  13303  isnsgrp  13313  grpinvex  13417  dfgrp2  13434  grpidinv2  13465  grpidinv  13466  dfgrp3mlem  13505  grp1  13513  imasgrp2  13521  dvdsrd  13931  opprunitd  13947  subrgdvds  14072  lss1d  14220  lspsn  14253  ellspsn  14254  rspsn  14371  znf1o  14488  basis2  14595  eltg2  14600  tg2  14607  neival  14690  isnei  14691  isneip  14693  restbasg  14715  cnpval  14745  iscnp  14746  icnpimaex  14758  lmbr  14760  lmbr2  14761  cnptoprest2  14787  lmff  14796  txbas  14805  txcnp  14818  txrest  14823  blssps  14974  blss  14975  mopni  15029  metss  15041  metrest  15053  metcnp3  15058  divcnap  15112  cncfval  15119  elcncf2  15121  cncfmet  15139  dedekindeulemuub  15164  dedekindeulemloc  15166  dedekindeulemlu  15168  suplociccreex  15171  dedekindicclemuub  15173  dedekindicclemloc  15175  dedekindicclemlu  15177  ivthreinc  15192  limccl  15206  ellimc3apf  15207  limcdifap  15209  limcmpted  15210  plyval  15279  elply2  15282  2lgslem1b  15641  bj-inf2vnlem1  16044  bj-inf2vnlem2  16045  bj-nn0sucALT  16052  sscoll2  16062  subctctexmid  16078  pw1nct  16081  isomninnlem  16110  trilpolemlt1  16121  trirec0  16124  ismkvnnlem  16132