Theorem ralbidv 1655

Description: Formula-building rule for restricted universal quantifier (deduction rule).

Hypothesis

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

Assertion

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

Distinct variable group:   ph,x

Proof of Theorem ralbidv

Step	Hyp	Ref	Expression
1		ax-17 968	. 2 |- (ph -> A.xph)
2		ralbidv.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	ralbid 1653	1 |- (ph -> (A.x e. A ps <-> A.x e. A ch))

Syntax hints:   -> wi 3   <-> wb 146  A.wral 1637

This theorem is referenced by:  2ralbidv 1672  rexralbidv 1674  raleqd 1783  raleq12d 1786  cbvral2v 1794  rcla42v 1871  rcla43v 1873  reu7 1925  sbcralt 1980  sbcralgf 1982  raaan 2350  elintg 2531  elintrabg 2536  eliin 2561  poeq1 2833  dffr2 2909  wereu 2935  onssmin 2998  ralxpf 3210  cnvpo 3508  funcnvuni 3550  dff3 3803  f1fvf 3860  isowe 3888  f1oweALT 3891  tfrlem3 3898  tfrlem12 3907  rdgeq1 3919  rdgeq2 3920  tz7.48lem 3940  elixp2 4333  nneneq 4492  supeq1 4549  supmo 4550  supub 4554  suplub 4555  suppr 4562  supsnALT 4564  zfregcl 4567  unbnnt 4611  rankval3 4653  unbndrank 4655  rankuni2 4662  rankun 4663  scottex 4688  scottexs 4690  scott0s 4691  bnd2 4696  hta 4700  aceq4 4706  aceq5lem5 4711  aceq5 4712  aceq6a 4713  aceq6b 4714  kmlem2 4738  kmlem13 4749  zorn2lem2 4761  zorn2lem7 4766  zorn2 4768  brdom3 4773  brdom7disj 4776  brdom6disj 4777  unidomg 4781  alephval2 4874  alephval3 4875  cflem 4877  cflecard 4884  cfeq0 4886  cfsuc 4887  nnleltp1t 5901  lbreu 5992  lble 5994  lbinfm 5995  sup2 5998  infm3 6001  infmsup 6015  infmrcl 6016  xrsupsslem 6023  xrinfmsslem 6024  xrsupss 6025  xrinfmss 6026  supxr 6028  supxrre 6030  uzwo4OLD 6158  uzwo5OLD 6159  uzwo3lem2 6165  uzwo3 6166  zmax 6168  flval2t 6181  flval3t 6182  iccsupr 6331  uzwo 6387  uzwoOLD 6388  uzinfm 6394  fsequb 6455  sqrlem6 6608  sqr2irrlem3 6656  seq1bnd 6847  cau3i 6851  cau3ir 6852  cvg1 6858  cvg3 6860  cvganz 6861  caubnd 6863  faclbnd4lem4 6888  bccl2t 6909  clim 6915  csbfsum 6965  clm3 7017  clm4 7018  clm0 7021  clm0nns 7023  clm4at 7028  climfnn 7030  climconst 7031  climshft 7041  climaddlem3 7052  climmullem8 7063  climmulc2 7065  caucvglem2 7094  caucvglem5 7097  caucvg3t 7104  serzf0 7105  ser1f0 7106  ser1clim0 7109  cvgcmp2lem 7116  cvgcmpub 7121  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  cvgcmp3cet 7126  expcnvlem1 7162  expcnvlem6 7167  cncfval 7199  negfcncf 7204  elcncf1d 7205  ivthlem8 7223  ivthlem4OLD 7228  ivthlem8OLD 7232  efaddlem25 7304  acdc3 7429  acdc2 7432  acdc5 7435  acdc 7437  infpn2 7452  ruclem33 7485  cnfval 7696  cnpfval 7697  iscn 7698  cnpval 7699  iscnp 7700  ismet 7737  ismsg 7739  msflem 7742  opnfval 7797  metcnp2 7827  metcnpi 7829  metcnpi2 7830  metcnpi3 7831  metcnpi4 7832  metcni 7833  metcni2 7834  metcnp3 7835  metcnss 7837  cncfmet 7844  lmfval 7863  caufval 7864  lmbr 7866  lmbrf 7868  lmconst 7872  lmnn 7873  iscau 7874  iscauf 7877  iscau5 7878  lmss 7888  causs 7890  lmclim 7898  metcnp4 7904  metcn4i 7906  xplm 7909  xpcn 7910  iscms2lem4 7926  cncms 7932  isgrp 7975  isgrpi 7976  grpideu 7987  grpidinv2 7994  cnid 8064  mulid 8069  isring 8078  ringi 8079  cnring 8099  ringsn 8100  vci 8104  isvcgOLD 8133  isvclem 8134  isnvlem 8167  isnvgOLD 8168  nvi 8173  nmcnilem 8272  va1cnlem 8279  sm1cnilem 8281  lnoval 8347  islno 8348  nmobndi 8370  isblo3i 8392  blo3i 8393  blocnilem 8395  blocni 8396  ajfval 8400  isphg 8407  ubthlem1 8460  ubthlem14 8473  ubthi 8475  minveclem10 8485  minveclem39 8518  htthlem7 8556  spwval2 8577  spwmo 8580  pilem2 8591  pilem3 8592  h2hcau 8788  h2hlm 8789  hilid 8949  hcau 8972  hcau2 8976  hlim 8977  hlim2 8981  hhcms 8993  sh 8999  hlim0 9026  ch2 9035  hhsscms 9067  ocelt 9070  occllem8 9096  projlem8 9109  pjth 9148  adjsymt 9676  elcnopt 9700  ellnopt 9701  elcnfnt 9726  ellnfnt 9727  cnopct 9753  cnfnct 9770  adjvalvalt 9777  0cnop 9819  0cnfn 9820  idcnop 9821  lnopeqt 9849  elunop2t 9853  lnophmt 9859  lnopcon 9878  lnopcont 9879  lnopcnbdt 9880  lnfncon 9905  lnfncont 9906  lnfncnbdt 9907  riesz3 9910  riesz4 9911  riesz4t 9912  riesz1t 9913  cnlnadjlem2 9916  cnlnadjlem4 9918  cnlnadjlem5 9919  cnlnadjlem8 9922  cnlnadj 9924  nmopadjle 9936  cnvbravalt 9956  leopg 9967  leoppost 9971  stelt 10051  mdbrt 10131  dmdbrt 10136  cdj3 10273  ghomgrpilem1 10290  homeofval 10403  ishomeo 10404  cnvhmphb 10413  cnvhmph 10414  hmeogrp 10425  isded 10513  dedi 10514  iscat 10531  cati 10532  ismona 10579  isfunb 10593

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972

This theorem depends on definitions:  df-bi 147  df-an 225  df-ral 1641

Copyright terms: Public domain