Theorem rcla4v 1876

Description: Restricted specialization with implicit substitution.

Hypothesis

Ref	Expression
rcla4v.1	⊢ (x = A → (φ ↔ ψ))

Assertion

Ref	Expression
rcla4v	⊢ (A ∈ B → (∀x ∈ B φ → ψ))

Distinct variable groups:   x,A   x,B   ψ,x

Proof of Theorem rcla4v

Step	Hyp	Ref	Expression
1		ax-17 973	. 2 ⊢ (ψ → ∀xψ)
2		rcla4v.1	. 2 ⊢ (x = A → (φ ↔ ψ))
3	1, 2	rcla4 1874	1 ⊢ (A ∈ B → (∀x ∈ B φ → ψ))

Syntax hints:   → wi 3   ↔ wb 146   = wceq 958   ∈ wcel 960  ∀wral 1648

This theorem is referenced by:  rcla4cv 1877  rcla4va 1878  rcla4dv 1881  rcla42v 1883  rcla43v 1885  intmin 2557  ralxfr 2905  wereu 2951  limuni3 3129  tfinds 3167  funcnvuni 3570  tfrlem2 3918  tz7.49 3965  oeordi 4220  nneneq 4518  unblem2 4552  unbnn2 4556  supub 4589  suplub 4590  rankun 4701  aceq3lem 4742  aceq5 4750  ac6lem 4764  numthlem 4793  unidom 4818  carduni 4869  alephval2 4913  cflim 4921  squeeze0 5926  nnleltp1t 5956  lbreu 6047  xrub 6082  dfuz 6204  uzwo5OLD 6213  uzwo3lem2 6219  zmax 6222  zbtwnre 6223  fzrevralt 6520  fsequb 6524  recant 6905  caubnd 6926  faclbnd4lem4 6951  bccl2t 6971  clm4le 7081  clmi1 7086  2climnn 7102  2climnn0 7103  climshft 7104  iserzshft2 7107  climaddlem3 7116  climmullem8 7127  climubi 7153  climcau 7156  caucvglem2 7158  caucvg 7163  serzf0 7169  ser1f0 7170  cvgratlem1ALT 7247  cvgratlem1 7250  cvgratlem4 7253  ivthlem6 7286  ivthlem7 7287  dsupivthlem 7291  unbenlem 7505  basgen2t 7638  clsval2 7682  metcnp 7884  lmle 7957  metelcls 7962  metcnp4 7967  metcn4i 7969  bcthlem2 7997  bcthlem16 8011  bcthlem17 8012  bcthlem33 8028  isgrp 8038  blocnilem 8460  ip2eqi 8513  minveclem27 8567  spwmo 8652  hial0 8963  hial02 8964  hial2eqt 8967  hlimunii 9103  ocorth 9159  occllem5 9172  projlem22 9202  projlem26 9206  h1de2 9471  pjjs 9640  lnopunilem1 9930  lnophmlem1 9936  nmcopexlem6 9951  nmcfnexlem6 9980  nlelch 9989  riesz4 9991  hmopidmch 10074  stge0t 10146  stle1t 10147  mdit 10217  mdbr3 10219  mdbr4 10220  dmdit 10224  dmdbr3 10227  dmdbr4 10228  dmdi4 10229  mdslmd1 10251  atss 10268  atom1d 10275  atmd 10321  sumdmdlem2 10341  cdj1 10355  cdj3 10363  ghomgrpilem1 10380  ghomf1olem 10391  cmphmp 10507  homcard 10525  cnfilca 10562

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-ral 1652  df-v 1815

Copyright terms: Public domain