Theorem rexbidv 2534

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

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-rex 2517

This theorem is referenced by:  rexbii  2540  2rexbidv  2558  rexralbidv  2559  rexeqbi1dv  2744  rexeqbidv  2748  cbvrex2vw  2780  cbvrex2v  2782  rspc2ev  2926  rspc3ev  2928  ceqsrex2v  2939  sbcrext  3110  uniiunlem  3318  eliun  3979  dfiin2g  4008  dfiunv2  4011  nn0suc  4708  rexxpf  4883  elrnmpt  4987  elrnmptg  4990  elimag  5086  funcnvuni  5406  fun11iun  5613  fvelrnb  5702  fvelimab  5711  foco2  5904  elabrex  5908  elabrexg  5909  abrexco  5910  f1oiso  5977  f1oiso2  5978  acexmidlemab  6022  acexmidlemcase  6023  abrexex2g  6291  abrexex2  6295  recseq  6515  tfr0dm  6531  tfr1onlemaccex  6557  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllemaccex  6570  tfrcllemres  6571  freceq1  6601  frec0g  6606  freccllem  6611  frecfcllem  6613  frecsuclem  6615  frecsuc  6616  nnaordex  6739  qseq2  6796  elqsg  6797  elixpsn  6947  ixpsnf1o  6948  isfi  6977  enfi  7103  fimax2gtri  7134  elfi  7213  supeq3  7232  supmoti  7235  suplubti  7242  supisolem  7250  cnvinfex  7260  eqinfti  7262  infvalti  7264  infglbti  7267  enomnilem  7380  finomni  7382  exmidomni  7384  fodjum  7388  fodju0  7389  fodjuomnilemres  7390  fodjuomni  7391  ismkvnex  7397  fodjumkvlemres  7401  fodjumkv  7402  enmkvlem  7403  ltexnqq  7671  elinp  7737  prnmaxl  7751  prnminu  7752  prarloclem3  7760  ltdfpr  7769  genpdflem  7770  genipv  7772  genpassl  7787  genpassu  7788  ltexprlemm  7863  ltexprlemloc  7870  cauappcvgprlemm  7908  cauappcvgprlemopl  7909  cauappcvgprlemlol  7910  cauappcvgprlemopu  7911  cauappcvgprlemupu  7912  cauappcvgprlemdisj  7914  cauappcvgprlemloc  7915  cauappcvgprlemladdfu  7917  cauappcvgprlemladdfl  7918  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  cauappcvgprlem1  7922  cauappcvgprlem2  7923  caucvgprlemm  7931  caucvgprlemopl  7932  caucvgprlemlol  7933  caucvgprlemopu  7934  caucvgprlemupu  7935  caucvgprlemdisj  7937  caucvgprlemloc  7938  caucvgprlemladdfu  7940  caucvgprlemladdrl  7941  caucvgprlem1  7942  caucvgprlem2  7943  caucvgprprlemell  7948  caucvgprprlemelu  7949  caucvgprprlemml  7957  caucvgprprlemmu  7958  caucvgprprlemexbt  7969  caucvgprprlem2  7973  suplocexprlemmu  7981  suplocexprlemru  7982  suplocexprlemdisj  7983  suplocexprlemloc  7984  suplocexprlemub  7986  recexgt0sr  8036  archsr  8045  map2psrprg  8068  suplocsrlemb  8069  axprecex  8143  nntopi  8157  axpre-suploclemres  8164  axpre-suploc  8165  cnegex  8399  apreap  8809  recexap  8875  sup3exmid  9179  creur  9181  creui  9182  cju  9183  supinfneg  9873  infsupneg  9874  infssuzex  10539  nninfdcex  10543  exbtwnzlemshrink  10554  rebtwn2zlemshrink  10559  modqmuladd  10674  hashunlem  11113  iswrd  11164  csbwrdg  11192  shftfvalg  11441  shftfval  11444  rexfiuz  11612  recvguniq  11618  fimaxre2  11850  clim  11904  sumeq1  11978  summodc  12007  fsum3  12011  mertenslemub  12158  mertenslemi1  12159  mertenslem2  12160  mertensabs  12161  prodeq1f  12176  prodeq2w  12180  prodmodc  12202  fprodseq  12207  divides  12413  odd2np1lem  12496  opeo  12521  omeo  12522  divalglemeunn  12545  divalglemeuneg  12547  zeqzmulgcd  12604  bezoutlemnewy  12630  bezoutlemmain  12632  bezoutlemex  12635  bezoutlemaz  12637  exprmfct  12773  nnnn0modprm0  12891  pceu  12931  pcprmpw2  12969  4sqlemafi  13031  4sqexercise1  13034  4sqlem12  13038  ennnfoneleminc  13095  ennnfonelemex  13098  ennnfonelemhom  13099  ennnfonelemnn0  13106  ennnfonelemr  13107  ctinfomlemom  13111  ctinfom  13112  nninfdclemcl  13132  nninfdclemp1  13134  nninfdc  13137  ptex  13410  grpinvalem  13531  igsumvalx  13535  gsumpropd  13538  gsumress  13541  gsum0g  13542  isnsgrp  13552  grpinvex  13656  dfgrp2  13673  grpidinv2  13704  grpidinv  13705  dfgrp3mlem  13744  grp1  13752  imasgrp2  13760  dvdsrd  14172  opprunitd  14188  subrgdvds  14313  lss1d  14462  lspsn  14495  ellspsn  14496  rspsn  14613  znf1o  14730  basis2  14842  eltg2  14847  tg2  14854  neival  14937  isnei  14938  isneip  14940  restbasg  14962  cnpval  14992  iscnp  14993  icnpimaex  15005  lmbr  15007  lmbr2  15008  cnptoprest2  15034  lmff  15043  txbas  15052  txcnp  15065  txrest  15070  blssps  15221  blss  15222  mopni  15276  metss  15288  metrest  15300  metcnp3  15305  divcnap  15359  cncfval  15366  elcncf2  15368  cncfmet  15386  dedekindeulemuub  15411  dedekindeulemloc  15413  dedekindeulemlu  15415  suplociccreex  15418  dedekindicclemuub  15420  dedekindicclemloc  15422  dedekindicclemlu  15424  ivthreinc  15439  limccl  15453  ellimc3apf  15454  limcdifap  15456  limcmpted  15457  plyval  15526  elply2  15529  2lgslem1b  15891  upgredg2vtx  16072  usgredg4  16139  ushgredgedg  16150  ushgredgedgloop  16152  vtxd0nedgbfi  16223  bj-inf2vnlem1  16669  bj-inf2vnlem2  16670  bj-nn0sucALT  16677  sscoll2  16687  3dom  16691  subctctexmid  16705  pw1nct  16708  isomninnlem  16745  trilpolemlt1  16756  trirec0  16759  qdiff  16764  ismkvnnlem  16768