Theorem rexbidv 2495

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-rex 2478

This theorem is referenced by:  rexbii  2501  2rexbidv  2519  rexralbidv  2520  rexeqbi1dv  2703  rexeqbidv  2707  cbvrex2vw  2738  cbvrex2v  2740  rspc2ev  2879  rspc3ev  2881  ceqsrex2v  2892  sbcrext  3063  uniiunlem  3268  eliun  3916  dfiin2g  3945  dfiunv2  3948  nn0suc  4636  rexxpf  4809  elrnmpt  4911  elrnmptg  4914  elimag  5009  funcnvuni  5323  fun11iun  5521  fvelrnb  5604  fvelimab  5613  foco2  5796  elabrex  5800  elabrexg  5801  abrexco  5802  f1oiso  5869  f1oiso2  5870  acexmidlemab  5912  acexmidlemcase  5913  abrexex2g  6172  abrexex2  6176  recseq  6359  tfr0dm  6375  tfr1onlemaccex  6401  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllemaccex  6414  tfrcllemres  6415  freceq1  6445  frec0g  6450  freccllem  6455  frecfcllem  6457  frecsuclem  6459  frecsuc  6460  nnaordex  6581  qseq2  6638  elqsg  6639  elixpsn  6789  ixpsnf1o  6790  isfi  6815  enfi  6929  fimax2gtri  6957  elfi  7030  supeq3  7049  supmoti  7052  suplubti  7059  supisolem  7067  cnvinfex  7077  eqinfti  7079  infvalti  7081  infglbti  7084  enomnilem  7197  finomni  7199  exmidomni  7201  fodjum  7205  fodju0  7206  fodjuomnilemres  7207  fodjuomni  7208  ismkvnex  7214  fodjumkvlemres  7218  fodjumkv  7219  enmkvlem  7220  ltexnqq  7468  elinp  7534  prnmaxl  7548  prnminu  7549  prarloclem3  7557  ltdfpr  7566  genpdflem  7567  genipv  7569  genpassl  7584  genpassu  7585  ltexprlemm  7660  ltexprlemloc  7667  cauappcvgprlemm  7705  cauappcvgprlemopl  7706  cauappcvgprlemlol  7707  cauappcvgprlemopu  7708  cauappcvgprlemupu  7709  cauappcvgprlemdisj  7711  cauappcvgprlemloc  7712  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  cauappcvgprlem1  7719  cauappcvgprlem2  7720  caucvgprlemm  7728  caucvgprlemopl  7729  caucvgprlemlol  7730  caucvgprlemopu  7731  caucvgprlemupu  7732  caucvgprlemdisj  7734  caucvgprlemloc  7735  caucvgprlemladdfu  7737  caucvgprlemladdrl  7738  caucvgprlem1  7739  caucvgprlem2  7740  caucvgprprlemell  7745  caucvgprprlemelu  7746  caucvgprprlemml  7754  caucvgprprlemmu  7755  caucvgprprlemexbt  7766  caucvgprprlem2  7770  suplocexprlemmu  7778  suplocexprlemru  7779  suplocexprlemdisj  7780  suplocexprlemloc  7781  suplocexprlemub  7783  recexgt0sr  7833  archsr  7842  map2psrprg  7865  suplocsrlemb  7866  axprecex  7940  nntopi  7954  axpre-suploclemres  7961  axpre-suploc  7962  cnegex  8197  apreap  8606  recexap  8672  sup3exmid  8976  creur  8978  creui  8979  cju  8980  supinfneg  9660  infsupneg  9661  exbtwnzlemshrink  10317  rebtwn2zlemshrink  10322  modqmuladd  10437  hashunlem  10875  iswrd  10916  csbwrdg  10943  shftfvalg  10962  shftfval  10965  rexfiuz  11133  recvguniq  11139  fimaxre2  11370  clim  11424  sumeq1  11498  summodc  11526  fsum3  11530  mertenslemub  11677  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  prodeq1f  11695  prodeq2w  11699  prodmodc  11721  fprodseq  11726  divides  11932  odd2np1lem  12013  opeo  12038  omeo  12039  divalglemeunn  12062  divalglemeuneg  12064  infssuzex  12086  nninfdcex  12090  zeqzmulgcd  12107  bezoutlemnewy  12133  bezoutlemmain  12135  bezoutlemex  12138  bezoutlemaz  12140  exprmfct  12276  nnnn0modprm0  12393  pceu  12433  pcprmpw2  12471  4sqlemafi  12533  4sqexercise1  12536  4sqlem12  12540  ennnfoneleminc  12568  ennnfonelemex  12571  ennnfonelemhom  12572  ennnfonelemnn0  12579  ennnfonelemr  12580  ctinfomlemom  12584  ctinfom  12585  nninfdclemcl  12605  nninfdclemp1  12607  nninfdc  12610  ptex  12875  grpinvalem  12968  igsumvalx  12972  gsumpropd  12975  gsumress  12978  gsum0g  12979  isnsgrp  12989  grpinvex  13082  dfgrp2  13099  grpidinv2  13130  grpidinv  13131  dfgrp3mlem  13170  grp1  13178  imasgrp2  13180  dvdsrd  13590  opprunitd  13606  subrgdvds  13731  lss1d  13879  lspsn  13912  ellspsn  13913  rspsn  14030  znf1o  14139  basis2  14216  eltg2  14221  tg2  14228  neival  14311  isnei  14312  isneip  14314  restbasg  14336  cnpval  14366  iscnp  14367  icnpimaex  14379  lmbr  14381  lmbr2  14382  cnptoprest2  14408  lmff  14417  txbas  14426  txcnp  14439  txrest  14444  blssps  14595  blss  14596  mopni  14650  metss  14662  metrest  14674  metcnp3  14679  divcnap  14723  cncfval  14727  elcncf2  14729  cncfmet  14747  dedekindeulemuub  14771  dedekindeulemloc  14773  dedekindeulemlu  14775  suplociccreex  14778  dedekindicclemuub  14780  dedekindicclemloc  14782  dedekindicclemlu  14784  ivthreinc  14799  limccl  14813  ellimc3apf  14814  limcdifap  14816  limcmpted  14817  plyval  14878  elply2  14881  bj-inf2vnlem1  15462  bj-inf2vnlem2  15463  bj-nn0sucALT  15470  sscoll2  15480  subctctexmid  15491  pw1nct  15493  isomninnlem  15520  trilpolemlt1  15531  trirec0  15534  ismkvnnlem  15542