Theorem rexbidv 2498

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

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-rex 2481

This theorem is referenced by:  rexbii  2504  2rexbidv  2522  rexralbidv  2523  rexeqbi1dv  2706  rexeqbidv  2710  cbvrex2vw  2741  cbvrex2v  2743  rspc2ev  2883  rspc3ev  2885  ceqsrex2v  2896  sbcrext  3067  uniiunlem  3273  eliun  3921  dfiin2g  3950  dfiunv2  3953  nn0suc  4641  rexxpf  4814  elrnmpt  4916  elrnmptg  4919  elimag  5014  funcnvuni  5328  fun11iun  5528  fvelrnb  5611  fvelimab  5620  foco2  5803  elabrex  5807  elabrexg  5808  abrexco  5809  f1oiso  5876  f1oiso2  5877  acexmidlemab  5919  acexmidlemcase  5920  abrexex2g  6186  abrexex2  6190  recseq  6373  tfr0dm  6389  tfr1onlemaccex  6415  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllemaccex  6428  tfrcllemres  6429  freceq1  6459  frec0g  6464  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecsuc  6474  nnaordex  6595  qseq2  6652  elqsg  6653  elixpsn  6803  ixpsnf1o  6804  isfi  6829  enfi  6943  fimax2gtri  6971  elfi  7046  supeq3  7065  supmoti  7068  suplubti  7075  supisolem  7083  cnvinfex  7093  eqinfti  7095  infvalti  7097  infglbti  7100  enomnilem  7213  finomni  7215  exmidomni  7217  fodjum  7221  fodju0  7222  fodjuomnilemres  7223  fodjuomni  7224  ismkvnex  7230  fodjumkvlemres  7234  fodjumkv  7235  enmkvlem  7236  ltexnqq  7494  elinp  7560  prnmaxl  7574  prnminu  7575  prarloclem3  7583  ltdfpr  7592  genpdflem  7593  genipv  7595  genpassl  7610  genpassu  7611  ltexprlemm  7686  ltexprlemloc  7693  cauappcvgprlemm  7731  cauappcvgprlemopl  7732  cauappcvgprlemlol  7733  cauappcvgprlemopu  7734  cauappcvgprlemupu  7735  cauappcvgprlemdisj  7737  cauappcvgprlemloc  7738  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  cauappcvgprlem1  7745  cauappcvgprlem2  7746  caucvgprlemm  7754  caucvgprlemopl  7755  caucvgprlemlol  7756  caucvgprlemopu  7757  caucvgprlemupu  7758  caucvgprlemdisj  7760  caucvgprlemloc  7761  caucvgprlemladdfu  7763  caucvgprlemladdrl  7764  caucvgprlem1  7765  caucvgprlem2  7766  caucvgprprlemell  7771  caucvgprprlemelu  7772  caucvgprprlemml  7780  caucvgprprlemmu  7781  caucvgprprlemexbt  7792  caucvgprprlem2  7796  suplocexprlemmu  7804  suplocexprlemru  7805  suplocexprlemdisj  7806  suplocexprlemloc  7807  suplocexprlemub  7809  recexgt0sr  7859  archsr  7868  map2psrprg  7891  suplocsrlemb  7892  axprecex  7966  nntopi  7980  axpre-suploclemres  7987  axpre-suploc  7988  cnegex  8223  apreap  8633  recexap  8699  sup3exmid  9003  creur  9005  creui  9006  cju  9007  supinfneg  9688  infsupneg  9689  infssuzex  10342  nninfdcex  10346  exbtwnzlemshrink  10357  rebtwn2zlemshrink  10362  modqmuladd  10477  hashunlem  10915  iswrd  10956  csbwrdg  10983  shftfvalg  11002  shftfval  11005  rexfiuz  11173  recvguniq  11179  fimaxre2  11411  clim  11465  sumeq1  11539  summodc  11567  fsum3  11571  mertenslemub  11718  mertenslemi1  11719  mertenslem2  11720  mertensabs  11721  prodeq1f  11736  prodeq2w  11740  prodmodc  11762  fprodseq  11767  divides  11973  odd2np1lem  12056  opeo  12081  omeo  12082  divalglemeunn  12105  divalglemeuneg  12107  zeqzmulgcd  12164  bezoutlemnewy  12190  bezoutlemmain  12192  bezoutlemex  12195  bezoutlemaz  12197  exprmfct  12333  nnnn0modprm0  12451  pceu  12491  pcprmpw2  12529  4sqlemafi  12591  4sqexercise1  12594  4sqlem12  12598  ennnfoneleminc  12655  ennnfonelemex  12658  ennnfonelemhom  12659  ennnfonelemnn0  12666  ennnfonelemr  12667  ctinfomlemom  12671  ctinfom  12672  nninfdclemcl  12692  nninfdclemp1  12694  nninfdc  12697  ptex  12968  grpinvalem  13089  igsumvalx  13093  gsumpropd  13096  gsumress  13099  gsum0g  13100  isnsgrp  13110  grpinvex  13214  dfgrp2  13231  grpidinv2  13262  grpidinv  13263  dfgrp3mlem  13302  grp1  13310  imasgrp2  13318  dvdsrd  13728  opprunitd  13744  subrgdvds  13869  lss1d  14017  lspsn  14050  ellspsn  14051  rspsn  14168  znf1o  14285  basis2  14392  eltg2  14397  tg2  14404  neival  14487  isnei  14488  isneip  14490  restbasg  14512  cnpval  14542  iscnp  14543  icnpimaex  14555  lmbr  14557  lmbr2  14558  cnptoprest2  14584  lmff  14593  txbas  14602  txcnp  14615  txrest  14620  blssps  14771  blss  14772  mopni  14826  metss  14838  metrest  14850  metcnp3  14855  divcnap  14909  cncfval  14916  elcncf2  14918  cncfmet  14936  dedekindeulemuub  14961  dedekindeulemloc  14963  dedekindeulemlu  14965  suplociccreex  14968  dedekindicclemuub  14970  dedekindicclemloc  14972  dedekindicclemlu  14974  ivthreinc  14989  limccl  15003  ellimc3apf  15004  limcdifap  15006  limcmpted  15007  plyval  15076  elply2  15079  2lgslem1b  15438  bj-inf2vnlem1  15724  bj-inf2vnlem2  15725  bj-nn0sucALT  15732  sscoll2  15742  subctctexmid  15755  pw1nct  15758  isomninnlem  15787  trilpolemlt1  15798  trirec0  15801  ismkvnnlem  15809