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  3968  dfiin2g  3997  dfiunv2  4000  nn0suc  4695  rexxpf  4868  elrnmpt  4972  elrnmptg  4975  elimag  5071  funcnvuni  5389  fun11iun  5592  fvelrnb  5680  fvelimab  5689  foco2  5876  elabrex  5880  elabrexg  5881  abrexco  5882  f1oiso  5949  f1oiso2  5950  acexmidlemab  5994  acexmidlemcase  5995  abrexex2g  6263  abrexex2  6267  recseq  6450  tfr0dm  6466  tfr1onlemaccex  6492  tfrcllemsucaccv  6498  tfrcllembxssdm  6500  tfrcllemaccex  6505  tfrcllemres  6506  freceq1  6536  frec0g  6541  freccllem  6546  frecfcllem  6548  frecsuclem  6550  frecsuc  6551  nnaordex  6672  qseq2  6729  elqsg  6730  elixpsn  6880  ixpsnf1o  6881  isfi  6910  enfi  7031  fimax2gtri  7059  elfi  7134  supeq3  7153  supmoti  7156  suplubti  7163  supisolem  7171  cnvinfex  7181  eqinfti  7183  infvalti  7185  infglbti  7188  enomnilem  7301  finomni  7303  exmidomni  7305  fodjum  7309  fodju0  7310  fodjuomnilemres  7311  fodjuomni  7312  ismkvnex  7318  fodjumkvlemres  7322  fodjumkv  7323  enmkvlem  7324  ltexnqq  7591  elinp  7657  prnmaxl  7671  prnminu  7672  prarloclem3  7680  ltdfpr  7689  genpdflem  7690  genipv  7692  genpassl  7707  genpassu  7708  ltexprlemm  7783  ltexprlemloc  7790  cauappcvgprlemm  7828  cauappcvgprlemopl  7829  cauappcvgprlemlol  7830  cauappcvgprlemopu  7831  cauappcvgprlemupu  7832  cauappcvgprlemdisj  7834  cauappcvgprlemloc  7835  cauappcvgprlemladdfu  7837  cauappcvgprlemladdfl  7838  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  cauappcvgprlem1  7842  cauappcvgprlem2  7843  caucvgprlemm  7851  caucvgprlemopl  7852  caucvgprlemlol  7853  caucvgprlemopu  7854  caucvgprlemupu  7855  caucvgprlemdisj  7857  caucvgprlemloc  7858  caucvgprlemladdfu  7860  caucvgprlemladdrl  7861  caucvgprlem1  7862  caucvgprlem2  7863  caucvgprprlemell  7868  caucvgprprlemelu  7869  caucvgprprlemml  7877  caucvgprprlemmu  7878  caucvgprprlemexbt  7889  caucvgprprlem2  7893  suplocexprlemmu  7901  suplocexprlemru  7902  suplocexprlemdisj  7903  suplocexprlemloc  7904  suplocexprlemub  7906  recexgt0sr  7956  archsr  7965  map2psrprg  7988  suplocsrlemb  7989  axprecex  8063  nntopi  8077  axpre-suploclemres  8084  axpre-suploc  8085  cnegex  8320  apreap  8730  recexap  8796  sup3exmid  9100  creur  9102  creui  9103  cju  9104  supinfneg  9786  infsupneg  9787  infssuzex  10448  nninfdcex  10452  exbtwnzlemshrink  10463  rebtwn2zlemshrink  10468  modqmuladd  10583  hashunlem  11021  iswrd  11068  csbwrdg  11096  shftfvalg  11324  shftfval  11327  rexfiuz  11495  recvguniq  11501  fimaxre2  11733  clim  11787  sumeq1  11861  summodc  11889  fsum3  11893  mertenslemub  12040  mertenslemi1  12041  mertenslem2  12042  mertensabs  12043  prodeq1f  12058  prodeq2w  12062  prodmodc  12084  fprodseq  12089  divides  12295  odd2np1lem  12378  opeo  12403  omeo  12404  divalglemeunn  12427  divalglemeuneg  12429  zeqzmulgcd  12486  bezoutlemnewy  12512  bezoutlemmain  12514  bezoutlemex  12517  bezoutlemaz  12519  exprmfct  12655  nnnn0modprm0  12773  pceu  12813  pcprmpw2  12851  4sqlemafi  12913  4sqexercise1  12916  4sqlem12  12920  ennnfoneleminc  12977  ennnfonelemex  12980  ennnfonelemhom  12981  ennnfonelemnn0  12988  ennnfonelemr  12989  ctinfomlemom  12993  ctinfom  12994  nninfdclemcl  13014  nninfdclemp1  13016  nninfdc  13019  ptex  13292  grpinvalem  13413  igsumvalx  13417  gsumpropd  13420  gsumress  13423  gsum0g  13424  isnsgrp  13434  grpinvex  13538  dfgrp2  13555  grpidinv2  13586  grpidinv  13587  dfgrp3mlem  13626  grp1  13634  imasgrp2  13642  dvdsrd  14052  opprunitd  14068  subrgdvds  14193  lss1d  14341  lspsn  14374  ellspsn  14375  rspsn  14492  znf1o  14609  basis2  14716  eltg2  14721  tg2  14728  neival  14811  isnei  14812  isneip  14814  restbasg  14836  cnpval  14866  iscnp  14867  icnpimaex  14879  lmbr  14881  lmbr2  14882  cnptoprest2  14908  lmff  14917  txbas  14926  txcnp  14939  txrest  14944  blssps  15095  blss  15096  mopni  15150  metss  15162  metrest  15174  metcnp3  15179  divcnap  15233  cncfval  15240  elcncf2  15242  cncfmet  15260  dedekindeulemuub  15285  dedekindeulemloc  15287  dedekindeulemlu  15289  suplociccreex  15292  dedekindicclemuub  15294  dedekindicclemloc  15296  dedekindicclemlu  15298  ivthreinc  15313  limccl  15327  ellimc3apf  15328  limcdifap  15330  limcmpted  15331  plyval  15400  elply2  15403  2lgslem1b  15762  upgredg2vtx  15940  usgredg4  16007  ushgredgedg  16018  ushgredgedgloop  16020  bj-inf2vnlem1  16291  bj-inf2vnlem2  16292  bj-nn0sucALT  16299  sscoll2  16309  subctctexmid  16325  pw1nct  16328  isomninnlem  16357  trilpolemlt1  16368  trirec0  16371  ismkvnnlem  16379