Theorem rexbidv 2551

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105  ∃wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This proof depends on definitions:  df-bi 117  df-nf 1514  df-rex 2534

This theorem is used by:  rexbii  2557  2rexbidv  2575  rexralbidv  2576  rexeqbi1dv  2762  rexeqbidv  2766  cbvrex2vw  2798  cbvrex2v  2800  rspc2ev  2945  rspc3ev  2947  ceqsrex2v  2958  sbcrext  3129  uniiunlem  3338  eliun  4016  dfiin2g  4045  dfiunv2  4048  nn0suc  4751  rexxpf  4927  elrnmpt  5031  elrnmptg  5034  elimag  5130  funcnvuni  5450  fun11iun  5660  fvelrnb  5750  fvelimab  5759  foco2  5959  elabrex  5963  elabrexg  5964  abrexco  5965  f1oiso  6032  f1oiso2  6033  acexmidlemab  6079  acexmidlemcase  6080  abrexex2g  6349  abrexex2  6353  elabreximd  6356  recseq  6577  tfr0dm  6593  tfr1onlemaccex  6619  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllemaccex  6632  tfrcllemres  6633  freceq1  6663  frec0g  6668  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecsuc  6678  nnaordex  6801  qseq2  6858  elqsg  6859  elixpsn  7017  ixpsnf1o  7018  isfi  7047  enfi  7175  fimax2gtri  7206  elfi  7305  supeq3  7330  supmoti  7333  suplubti  7340  supisolem  7348  cnvinfex  7358  eqinfti  7360  infvalti  7362  infglbti  7365  enomnilem  7478  finomni  7480  exmidomni  7482  fodjum  7486  fodju0  7487  fodjuomnilemres  7488  fodjuomni  7489  ismkvnex  7495  fodjumkvlemres  7499  fodjumkv  7500  enmkvlem  7501  ltexnqq  7775  elinp  7841  prnmaxl  7855  prnminu  7856  prarloclem3  7864  ltdfpr  7873  genpdflem  7874  genipv  7876  genpassl  7891  genpassu  7892  ltexprlemm  7967  ltexprlemloc  7974  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemopu  8015  cauappcvgprlemupu  8016  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlem2  8027  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemopu  8038  caucvgprlemupu  8039  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprlem1  8046  caucvgprlem2  8047  caucvgprprlemell  8052  caucvgprprlemelu  8053  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemexbt  8073  caucvgprprlem2  8077  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemub  8090  recexgt0sr  8140  archsr  8149  map2psrprg  8172  suplocsrlemb  8173  axprecex  8247  nntopi  8261  axpre-suploclemres  8268  axpre-suploc  8269  cnegex  8505  apreap  8917  recexap  8983  sup3exmid  9289  creur  9291  creui  9292  cju  9293  supinfneg  10004  infsupneg  10005  infssuzex  10676  nninfdcex  10682  exbtwnzlemshrink  10693  rebtwn2zlemshrink  10698  modqmuladd  10816  hashunlem  11258  iswrd  11320  csbwrdg  11348  shftfvalg  11597  shftfval  11600  rexfiuz  11769  recvguniq  11775  fimaxre2  12008  clim  12063  sumeq1  12137  summodc  12166  fsum3  12170  mertenslemub  12317  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  prodeq1f  12335  prodeq2w  12339  prodmodc  12361  fprodseq  12366  divides  12572  odd2np1lem  12655  opeo  12680  omeo  12681  divalglemeunn  12704  divalglemeuneg  12706  zeqzmulgcd  12763  bezoutlemnewy  12789  bezoutlemmain  12791  bezoutlemex  12794  bezoutlemaz  12796  exprmfct  12933  nnnn0modprm0  13054  pceu  13094  pcprmpw2  13132  4sqlemafi  13194  4sqexercise1  13197  4sqlem12  13201  ennnfoneleminc  13351  ennnfonelemex  13354  ennnfonelemhom  13355  ennnfonelemnn0  13362  ennnfonelemr  13363  ctinfomlemom  13367  ctinfom  13368  nninfdclemcl  13388  nninfdclemp1  13390  nninfdc  13393  ptex  13667  grpinvalem  13754  gzsumvalx  13758  gzsumress  13761  gzsum0  13762  isnsgrp  13770  grpinvex  13864  dfgrp2  13881  grpidinv2  13912  grpidinv  13913  dfgrp3mlem  13952  grp1  13960  imasgrp2  13962  dvdsrd  14450  opprunitd  14466  subrgdvds  14592  lss1d  14769  lspsn  14802  ellspsn  14803  rspsn  14920  znf1o  15035  basis2  15198  eltg2  15203  tg2  15210  neival  15293  isnei  15294  isneip  15296  restbasg  15318  cnpval  15348  iscnp  15349  icnpimaex  15361  lmbr  15363  lmbr2  15364  cnptoprest2  15390  lmff  15399  txbas  15408  txcnp  15421  txrest  15426  blssps  15577  blss  15578  mopni  15632  metss  15644  metrest  15656  metcnp3  15661  divcnap  15715  cncfval  15722  elcncf2  15724  cncfmet  15742  dedekindeulemuub  15767  dedekindeulemloc  15769  dedekindeulemlu  15771  suplociccreex  15774  dedekindicclemuub  15776  dedekindicclemloc  15778  dedekindicclemlu  15780  ivthreinc  15795  limccl  15809  ellimc3apf  15810  limcdifap  15812  limcmpted  15813  plyval  15882  elply2  15885  2lgslem1b  16306  upgredg2vtx  16487  usgredg4  16554  ushgredgedg  16565  ushgredgedgloop  16567  vtxd0nedgbfi  16638  bj-inf2vnlem1  17094  bj-inf2vnlem2  17095  bj-nn0sucALT  17102  sscoll2  17112  3dom  17116  subctctexmid  17128  pw1nct  17131  isomninnlem  17177  trilpolemlt1  17188  trirec0  17191  qdiff  17196  ismkvnnlem  17200