Theorem rexbidv 2551

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 1581	. 2 |- F/ x ph
2		ralbidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	rexbid 2549	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   E.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  7331  supmoti  7334  suplubti  7341  supisolem  7349  cnvinfex  7359  eqinfti  7361  infvalti  7363  infglbti  7366  enomnilem  7479  finomni  7481  exmidomni  7483  fodjum  7487  fodju0  7488  fodjuomnilemres  7489  fodjuomni  7490  ismkvnex  7496  fodjumkvlemres  7500  fodjumkv  7501  enmkvlem  7502  ltexnqq  7776  elinp  7842  prnmaxl  7856  prnminu  7857  prarloclem3  7865  ltdfpr  7874  genpdflem  7875  genipv  7877  genpassl  7892  genpassu  7893  ltexprlemm  7968  ltexprlemloc  7975  cauappcvgprlemm  8013  cauappcvgprlemopl  8014  cauappcvgprlemlol  8015  cauappcvgprlemopu  8016  cauappcvgprlemupu  8017  cauappcvgprlemdisj  8019  cauappcvgprlemloc  8020  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  cauappcvgprlem1  8027  cauappcvgprlem2  8028  caucvgprlemm  8036  caucvgprlemopl  8037  caucvgprlemlol  8038  caucvgprlemopu  8039  caucvgprlemupu  8040  caucvgprlemdisj  8042  caucvgprlemloc  8043  caucvgprlemladdfu  8045  caucvgprlemladdrl  8046  caucvgprlem1  8047  caucvgprlem2  8048  caucvgprprlemell  8053  caucvgprprlemelu  8054  caucvgprprlemml  8062  caucvgprprlemmu  8063  caucvgprprlemexbt  8074  caucvgprprlem2  8078  suplocexprlemmu  8086  suplocexprlemru  8087  suplocexprlemdisj  8088  suplocexprlemloc  8089  suplocexprlemub  8091  recexgt0sr  8141  archsr  8150  map2psrprg  8173  suplocsrlemb  8174  axprecex  8248  nntopi  8262  axpre-suploclemres  8269  axpre-suploc  8270  cnegex  8506  apreap  8918  recexap  8984  sup3exmid  9290  creur  9292  creui  9293  cju  9294  supinfneg  10005  infsupneg  10006  infssuzex  10677  nninfdcex  10683  exbtwnzlemshrink  10694  rebtwn2zlemshrink  10699  modqmuladd  10818  hashunlem  11260  iswrd  11322  csbwrdg  11350  shftfvalg  11599  shftfval  11602  rexfiuz  11771  recvguniq  11777  fimaxre2  12010  fiidxsupcl  12012  clim  12066  sumeq1  12140  summodc  12169  fsum3  12173  mertenslemub  12320  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  prodeq1f  12338  prodeq2w  12342  prodmodc  12364  fprodseq  12369  divides  12575  odd2np1lem  12658  opeo  12683  omeo  12684  divalglemeunn  12707  divalglemeuneg  12709  zeqzmulgcd  12766  bezoutlemnewy  12792  bezoutlemmain  12794  bezoutlemex  12797  bezoutlemaz  12799  exprmfct  12936  nnnn0modprm0  13057  pceu  13097  pcprmpw2  13135  4sqlemafi  13197  4sqexercise1  13200  4sqlem12  13204  ennnfoneleminc  13354  ennnfonelemex  13357  ennnfonelemhom  13358  ennnfonelemnn0  13365  ennnfonelemr  13366  ctinfomlemom  13370  ctinfom  13371  nninfdclemcl  13391  nninfdclemp1  13393  nninfdc  13396  ptex  13671  grpinvalem  13758  gzsumvalx  13762  gzsumress  13765  gzsum0  13766  isnsgrp  13774  grpinvex  13868  dfgrp2  13885  grpidinv2  13916  grpidinv  13917  dfgrp3mlem  13956  grp1  13964  imasgrp2  13966  dvdsrd  14485  opprunitd  14501  subrgdvds  14627  lss1d  14804  lspsn  14837  ellspsn  14838  rspsn  14955  znf1o  15070  basis2  15240  eltg2  15245  tg2  15252  neival  15335  isnei  15336  isneip  15338  restbasg  15360  cnpval  15390  iscnp  15391  icnpimaex  15403  lmbr  15405  lmbr2  15406  cnptoprest2  15432  lmff  15441  txbas  15450  txcnp  15463  txrest  15468  blssps  15619  blss  15620  mopni  15674  metss  15686  metrest  15698  metcnp3  15703  divcnap  15757  cncfval  15764  elcncf2  15766  cncfmet  15784  dedekindeulemuub  15809  dedekindeulemloc  15811  dedekindeulemlu  15813  suplociccreex  15816  dedekindicclemuub  15818  dedekindicclemloc  15820  dedekindicclemlu  15822  ivthreinc  15837  limccl  15851  ellimc3apf  15852  limcdifap  15854  limcmpted  15855  plyval  15924  elply2  15927  2lgslem1b  16374  upgredg2vtx  16555  usgredg4  16622  ushgredgedg  16633  ushgredgedgloop  16635  vtxd0nedgbfi  16706  bj-inf2vnlem1  17162  bj-inf2vnlem2  17163  bj-nn0sucALT  17170  sscoll2  17180  3dom  17184  subctctexmid  17196  pw1nct  17199  isomninnlem  17245  trilpolemlt1  17257  trirec0  17260  qdiff  17265  ismkvnnlem  17269