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  2880  rspc3ev  2882  ceqsrex2v  2893  sbcrext  3064  uniiunlem  3269  eliun  3917  dfiin2g  3946  dfiunv2  3949  nn0suc  4637  rexxpf  4810  elrnmpt  4912  elrnmptg  4915  elimag  5010  funcnvuni  5324  fun11iun  5522  fvelrnb  5605  fvelimab  5614  foco2  5797  elabrex  5801  elabrexg  5802  abrexco  5803  f1oiso  5870  f1oiso2  5871  acexmidlemab  5913  acexmidlemcase  5914  abrexex2g  6174  abrexex2  6178  recseq  6361  tfr0dm  6377  tfr1onlemaccex  6403  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllemaccex  6416  tfrcllemres  6417  freceq1  6447  frec0g  6452  freccllem  6457  frecfcllem  6459  frecsuclem  6461  frecsuc  6462  nnaordex  6583  qseq2  6640  elqsg  6641  elixpsn  6791  ixpsnf1o  6792  isfi  6817  enfi  6931  fimax2gtri  6959  elfi  7032  supeq3  7051  supmoti  7054  suplubti  7061  supisolem  7069  cnvinfex  7079  eqinfti  7081  infvalti  7083  infglbti  7086  enomnilem  7199  finomni  7201  exmidomni  7203  fodjum  7207  fodju0  7208  fodjuomnilemres  7209  fodjuomni  7210  ismkvnex  7216  fodjumkvlemres  7220  fodjumkv  7221  enmkvlem  7222  ltexnqq  7470  elinp  7536  prnmaxl  7550  prnminu  7551  prarloclem3  7559  ltdfpr  7568  genpdflem  7569  genipv  7571  genpassl  7586  genpassu  7587  ltexprlemm  7662  ltexprlemloc  7669  cauappcvgprlemm  7707  cauappcvgprlemopl  7708  cauappcvgprlemlol  7709  cauappcvgprlemopu  7710  cauappcvgprlemupu  7711  cauappcvgprlemdisj  7713  cauappcvgprlemloc  7714  cauappcvgprlemladdfu  7716  cauappcvgprlemladdfl  7717  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  cauappcvgprlem1  7721  cauappcvgprlem2  7722  caucvgprlemm  7730  caucvgprlemopl  7731  caucvgprlemlol  7732  caucvgprlemopu  7733  caucvgprlemupu  7734  caucvgprlemdisj  7736  caucvgprlemloc  7737  caucvgprlemladdfu  7739  caucvgprlemladdrl  7740  caucvgprlem1  7741  caucvgprlem2  7742  caucvgprprlemell  7747  caucvgprprlemelu  7748  caucvgprprlemml  7756  caucvgprprlemmu  7757  caucvgprprlemexbt  7768  caucvgprprlem2  7772  suplocexprlemmu  7780  suplocexprlemru  7781  suplocexprlemdisj  7782  suplocexprlemloc  7783  suplocexprlemub  7785  recexgt0sr  7835  archsr  7844  map2psrprg  7867  suplocsrlemb  7868  axprecex  7942  nntopi  7956  axpre-suploclemres  7963  axpre-suploc  7964  cnegex  8199  apreap  8608  recexap  8674  sup3exmid  8978  creur  8980  creui  8981  cju  8982  supinfneg  9663  infsupneg  9664  exbtwnzlemshrink  10320  rebtwn2zlemshrink  10325  modqmuladd  10440  hashunlem  10878  iswrd  10919  csbwrdg  10946  shftfvalg  10965  shftfval  10968  rexfiuz  11136  recvguniq  11142  fimaxre2  11373  clim  11427  sumeq1  11501  summodc  11529  fsum3  11533  mertenslemub  11680  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  prodeq1f  11698  prodeq2w  11702  prodmodc  11724  fprodseq  11729  divides  11935  odd2np1lem  12016  opeo  12041  omeo  12042  divalglemeunn  12065  divalglemeuneg  12067  infssuzex  12089  nninfdcex  12093  zeqzmulgcd  12110  bezoutlemnewy  12136  bezoutlemmain  12138  bezoutlemex  12141  bezoutlemaz  12143  exprmfct  12279  nnnn0modprm0  12396  pceu  12436  pcprmpw2  12474  4sqlemafi  12536  4sqexercise1  12539  4sqlem12  12543  ennnfoneleminc  12571  ennnfonelemex  12574  ennnfonelemhom  12575  ennnfonelemnn0  12582  ennnfonelemr  12583  ctinfomlemom  12587  ctinfom  12588  nninfdclemcl  12608  nninfdclemp1  12610  nninfdc  12613  ptex  12878  grpinvalem  12971  igsumvalx  12975  gsumpropd  12978  gsumress  12981  gsum0g  12982  isnsgrp  12992  grpinvex  13085  dfgrp2  13102  grpidinv2  13133  grpidinv  13134  dfgrp3mlem  13173  grp1  13181  imasgrp2  13183  dvdsrd  13593  opprunitd  13609  subrgdvds  13734  lss1d  13882  lspsn  13915  ellspsn  13916  rspsn  14033  znf1o  14150  basis2  14227  eltg2  14232  tg2  14239  neival  14322  isnei  14323  isneip  14325  restbasg  14347  cnpval  14377  iscnp  14378  icnpimaex  14390  lmbr  14392  lmbr2  14393  cnptoprest2  14419  lmff  14428  txbas  14437  txcnp  14450  txrest  14455  blssps  14606  blss  14607  mopni  14661  metss  14673  metrest  14685  metcnp3  14690  divcnap  14744  cncfval  14751  elcncf2  14753  cncfmet  14771  dedekindeulemuub  14796  dedekindeulemloc  14798  dedekindeulemlu  14800  suplociccreex  14803  dedekindicclemuub  14805  dedekindicclemloc  14807  dedekindicclemlu  14809  ivthreinc  14824  limccl  14838  ellimc3apf  14839  limcdifap  14841  limcmpted  14842  plyval  14911  elply2  14914  2lgslem1b  15246  bj-inf2vnlem1  15532  bj-inf2vnlem2  15533  bj-nn0sucALT  15540  sscoll2  15550  subctctexmid  15561  pw1nct  15563  isomninnlem  15590  trilpolemlt1  15601  trirec0  15604  ismkvnnlem  15612