Theorem rexbidv 2531

Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 20-Nov-1994.)

Hypothesis

Ref	Expression
ralbidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
rexbidv	|- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem rexbidv

Step	Hyp	Ref	Expression
1		nfv 1574	. 2 |- F/ x ph
2		ralbidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	rexbid 2529	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 105   E.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  3969  dfiin2g  3998  dfiunv2  4001  nn0suc  4696  rexxpf  4869  elrnmpt  4973  elrnmptg  4976  elimag  5072  funcnvuni  5390  fun11iun  5593  fvelrnb  5681  fvelimab  5690  foco2  5877  elabrex  5881  elabrexg  5882  abrexco  5883  f1oiso  5950  f1oiso2  5951  acexmidlemab  5995  acexmidlemcase  5996  abrexex2g  6265  abrexex2  6269  recseq  6452  tfr0dm  6468  tfr1onlemaccex  6494  tfrcllemsucaccv  6500  tfrcllembxssdm  6502  tfrcllemaccex  6507  tfrcllemres  6508  freceq1  6538  frec0g  6543  freccllem  6548  frecfcllem  6550  frecsuclem  6552  frecsuc  6553  nnaordex  6674  qseq2  6731  elqsg  6732  elixpsn  6882  ixpsnf1o  6883  isfi  6912  enfi  7035  fimax2gtri  7063  elfi  7138  supeq3  7157  supmoti  7160  suplubti  7167  supisolem  7175  cnvinfex  7185  eqinfti  7187  infvalti  7189  infglbti  7192  enomnilem  7305  finomni  7307  exmidomni  7309  fodjum  7313  fodju0  7314  fodjuomnilemres  7315  fodjuomni  7316  ismkvnex  7322  fodjumkvlemres  7326  fodjumkv  7327  enmkvlem  7328  ltexnqq  7595  elinp  7661  prnmaxl  7675  prnminu  7676  prarloclem3  7684  ltdfpr  7693  genpdflem  7694  genipv  7696  genpassl  7711  genpassu  7712  ltexprlemm  7787  ltexprlemloc  7794  cauappcvgprlemm  7832  cauappcvgprlemopl  7833  cauappcvgprlemlol  7834  cauappcvgprlemopu  7835  cauappcvgprlemupu  7836  cauappcvgprlemdisj  7838  cauappcvgprlemloc  7839  cauappcvgprlemladdfu  7841  cauappcvgprlemladdfl  7842  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  cauappcvgprlem1  7846  cauappcvgprlem2  7847  caucvgprlemm  7855  caucvgprlemopl  7856  caucvgprlemlol  7857  caucvgprlemopu  7858  caucvgprlemupu  7859  caucvgprlemdisj  7861  caucvgprlemloc  7862  caucvgprlemladdfu  7864  caucvgprlemladdrl  7865  caucvgprlem1  7866  caucvgprlem2  7867  caucvgprprlemell  7872  caucvgprprlemelu  7873  caucvgprprlemml  7881  caucvgprprlemmu  7882  caucvgprprlemexbt  7893  caucvgprprlem2  7897  suplocexprlemmu  7905  suplocexprlemru  7906  suplocexprlemdisj  7907  suplocexprlemloc  7908  suplocexprlemub  7910  recexgt0sr  7960  archsr  7969  map2psrprg  7992  suplocsrlemb  7993  axprecex  8067  nntopi  8081  axpre-suploclemres  8088  axpre-suploc  8089  cnegex  8324  apreap  8734  recexap  8800  sup3exmid  9104  creur  9106  creui  9107  cju  9108  supinfneg  9790  infsupneg  9791  infssuzex  10453  nninfdcex  10457  exbtwnzlemshrink  10468  rebtwn2zlemshrink  10473  modqmuladd  10588  hashunlem  11026  iswrd  11073  csbwrdg  11101  shftfvalg  11329  shftfval  11332  rexfiuz  11500  recvguniq  11506  fimaxre2  11738  clim  11792  sumeq1  11866  summodc  11894  fsum3  11898  mertenslemub  12045  mertenslemi1  12046  mertenslem2  12047  mertensabs  12048  prodeq1f  12063  prodeq2w  12067  prodmodc  12089  fprodseq  12094  divides  12300  odd2np1lem  12383  opeo  12408  omeo  12409  divalglemeunn  12432  divalglemeuneg  12434  zeqzmulgcd  12491  bezoutlemnewy  12517  bezoutlemmain  12519  bezoutlemex  12522  bezoutlemaz  12524  exprmfct  12660  nnnn0modprm0  12778  pceu  12818  pcprmpw2  12856  4sqlemafi  12918  4sqexercise1  12921  4sqlem12  12925  ennnfoneleminc  12982  ennnfonelemex  12985  ennnfonelemhom  12986  ennnfonelemnn0  12993  ennnfonelemr  12994  ctinfomlemom  12998  ctinfom  12999  nninfdclemcl  13019  nninfdclemp1  13021  nninfdc  13024  ptex  13297  grpinvalem  13418  igsumvalx  13422  gsumpropd  13425  gsumress  13428  gsum0g  13429  isnsgrp  13439  grpinvex  13543  dfgrp2  13560  grpidinv2  13591  grpidinv  13592  dfgrp3mlem  13631  grp1  13639  imasgrp2  13647  dvdsrd  14058  opprunitd  14074  subrgdvds  14199  lss1d  14347  lspsn  14380  ellspsn  14381  rspsn  14498  znf1o  14615  basis2  14722  eltg2  14727  tg2  14734  neival  14817  isnei  14818  isneip  14820  restbasg  14842  cnpval  14872  iscnp  14873  icnpimaex  14885  lmbr  14887  lmbr2  14888  cnptoprest2  14914  lmff  14923  txbas  14932  txcnp  14945  txrest  14950  blssps  15101  blss  15102  mopni  15156  metss  15168  metrest  15180  metcnp3  15185  divcnap  15239  cncfval  15246  elcncf2  15248  cncfmet  15266  dedekindeulemuub  15291  dedekindeulemloc  15293  dedekindeulemlu  15295  suplociccreex  15298  dedekindicclemuub  15300  dedekindicclemloc  15302  dedekindicclemlu  15304  ivthreinc  15319  limccl  15333  ellimc3apf  15334  limcdifap  15336  limcmpted  15337  plyval  15406  elply2  15409  2lgslem1b  15768  upgredg2vtx  15946  usgredg4  16013  ushgredgedg  16024  ushgredgedgloop  16026  bj-inf2vnlem1  16333  bj-inf2vnlem2  16334  bj-nn0sucALT  16341  sscoll2  16351  subctctexmid  16366  pw1nct  16369  isomninnlem  16398  trilpolemlt1  16409  trirec0  16412  ismkvnnlem  16420