Theorem ralbidv 1666

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

Hypothesis

Ref	Expression
ralbidv.1	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
ralbidv	⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ A χ))

Distinct variable group:   φ,x

Proof of Theorem ralbidv

Step	Hyp	Ref	Expression
1		ax-17 973	. 2 ⊢ (φ → ∀xφ)
2		ralbidv.1	. 2 ⊢ (φ → (ψ ↔ χ))
3	1, 2	ralbid 1664	1 ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ A χ))

Syntax hints:   → wi 3   ↔ wb 146  ∀wral 1648

This theorem is referenced by:  2ralbidv 1683  rexralbidv 1685  raleqd 1794  raleq12d 1797  cbvral2v 1806  rcla42v 1883  rcla43v 1885  reu7 1938  sbcralt 1993  sbcralgf 1995  raaan 2364  elintg 2545  elintrabg 2550  eliin 2575  poeq1 2848  dffr2 2925  wereu 2951  onssmin 3014  ralxpf 3226  cnvpo 3528  funcnvuni 3570  dff3 3824  f1fvf 3881  isowe 3909  f1oweALT 3912  tfrlem3 3919  tfrlem12 3928  rdgeq1 3940  rdgeq2 3941  tz7.48lem 3961  elixp2 4355  nneneq 4518  supeq1 4584  supmo 4585  supub 4589  suplub 4590  supmaxlem 4597  suppr 4599  supsnALT 4601  zfregcl 4604  unbnnt 4649  rankval3 4691  unbndrank 4693  rankuni2 4700  rankun 4701  scottex 4726  scottexs 4728  scott0s 4729  bnd2 4734  hta 4738  aceq4 4744  aceq5lem5 4749  aceq5 4750  aceq6a 4751  aceq6b 4752  kmlem2 4776  kmlem13 4787  zorn2lem2 4799  zorn2lem7 4804  zorn2 4806  brdom3 4811  brdom7disj 4814  brdom6disj 4815  unidomg 4819  alephval2 4913  alephval3 4914  cflem 4917  cflecard 4924  cfeq0 4926  cfsuc 4927  nnleltp1t 5956  lbreu 6047  lble 6049  lbinfm 6050  sup2 6053  infm3 6056  infmsup 6070  infmrcl 6071  xrsupsslem 6078  xrinfmsslem 6079  xrsupss 6080  xrinfmss 6081  supxr 6083  supxrre 6085  uzwo4OLD 6212  uzwo5OLD 6213  uzwo3lem2 6219  uzwo3 6220  zmax 6222  flval2t 6240  flval3t 6241  iccsupr 6399  uzwo 6456  uzwoOLD 6457  uzinfm 6463  fsequb 6524  sqrlem6 6679  sqr2irrlem3 6727  seq1bnd 6910  cau3i 6914  cau3ir 6915  cvg1 6921  cvg3 6923  cvganz 6924  caubnd 6926  faclbnd4lem4 6951  bccl2t 6971  clim 6977  csbfsum 7027  clm3 7079  clm4 7080  clm0 7083  clm0nns 7085  clm4at 7090  climfnn 7092  climconst 7094  climshft 7104  climabs0 7113  climaddlem3 7116  climmullem8 7127  climmulc2 7129  caucvglem2 7158  caucvglem5 7161  caucvg3t 7168  serzf0 7169  ser1f0 7170  ser1clim0 7173  cvgcmp2lem 7180  cvgcmpub 7185  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  cvgcmp3cet 7190  expcnvlem1 7227  expcnvlem6 7232  cncfval 7264  negfcncf 7269  elcncf1d 7270  ivthlem8 7288  efaddlem25 7362  acdc3 7488  acdc2 7491  acdc5 7494  acdc 7496  infpn2 7510  ruclem33 7543  cnfval 7753  cnpfval 7754  iscn 7755  cnpval 7756  iscnp 7757  iscnp2 7758  ismet 7795  ismsg 7797  msflem 7800  opnfval 7854  metcnp2 7885  metcnpi 7887  metcnpi2 7888  metcnpi3 7889  metcnpi4 7890  metcni 7891  metcni2 7892  metcnp3 7893  metcnss 7895  cncfmet 7902  lmfval 7922  caufval 7923  lmbr 7925  lmbrf 7927  lmconst 7931  lmnn 7932  iscau 7933  iscauf 7936  iscau5 7938  iscaunns 7941  lmss 7950  causs 7952  lmclim 7960  metcnp4 7967  metcn4i 7969  xplm 7972  xpcn 7973  iscms2lem4 7989  cncms 7995  isgrp 8038  isgrpi 8039  grpideu 8050  grpidinv2 8056  cnid 8123  mulid 8128  isring 8137  ringi 8138  cnring 8158  ringsn 8159  vci 8163  isvclem 8192  isnvlem 8225  nvi 8229  nmcnilem 8333  va1cnlem 8341  sm1cnilem 8343  lnoval 8409  islno 8410  nmobndi 8434  isblo3i 8457  blo3i 8458  blocnilem 8460  blocni 8461  ajfval 8465  isphg 8472  ubthlem1 8525  ubthlem14 8538  ubthi 8540  minveclem10 8550  minveclem39 8583  htthlem7 8622  spwval2 8649  spwmo 8652  spwpr2 8654  spwpr4OLD 8658  spwpr4aOLD 8659  pilem2 8667  pilem3 8668  h2hcau 8844  h2hlm 8845  hilid 9023  hcau 9046  hcau2 9050  hlim 9051  hlim2 9055  hhcms 9067  sh 9073  hlim0 9100  ch2 9109  hhsscms 9145  ocelt 9149  occllem8 9175  projlem8 9188  pjth 9228  adjsymt 9754  elcnopt 9778  ellnopt 9779  elcnfnt 9804  ellnfnt 9805  cnopct 9832  cnfnct 9849  adjvalvalt 9856  0cnop 9898  0cnfn 9899  idcnop 9900  lnopeqt 9929  elunop2t 9933  lnophmt 9939  lnopcon 9958  lnopcont 9959  lnopcnbdt 9960  lnfncon 9985  lnfncont 9986  lnfncnbdt 9987  riesz3 9990  riesz4 9991  riesz4t 9992  riesz1t 9993  cnlnadjlem2 9996  cnlnadjlem4 9998  cnlnadjlem5 9999  cnlnadjlem8 10002  cnlnadj 10004  nmopadjle 10016  cnvbravalt 10038  leopg 10050  leoppost 10054  stelt 10136  mdbrt 10216  dmdbrt 10221  cdj3 10363  ghomgrpilem1 10380  homeofval 10502  ishomeo 10503  cnvhmphb 10512  cnvhmph 10513  hmeogrp 10524  hmeobc 10528  isded 10640  dedi 10641  iscat 10658  cati 10659  ismona 10708  isepia 10718  isfunb 10726

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977

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

Copyright terms: Public domain