Theorem rcla4v 1919

Description: Restricted specialization, using implicit substitition.

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 1007	. 2 ⊢ (ψ → ∀xψ)
2		rcla4v.1	. 2 ⊢ (x = A → (φ ↔ ψ))
3	1, 2	rcla4 1917	1 ⊢ (A ∈ B → (∀x ∈ B φ → ψ))

Syntax hints:   → wi 3   ↔ wb 144   = wceq 992   ∈ wcel 994  ∀wral 1691

This theorem is referenced by:  rcla4cv 1920  rcla4va 1921  rcla4dv 1924  rcla42v 1926  rcla43v 1928  intmin 2620  wereu 2972  ralxfr 3122  limuni3 3206  tfinds 3212  funcnvuni 3669  tfrlem2 4213  tz7.49 4260  oeordi 4350  nneneq 4659  unblem2 4687  unbnn2 4691  supub 4723  suplub 4724  rankun 4837  aceq3lem 4878  aceq5 4886  ac6lem 4900  numthlem 4929  unidom 4954  carduni 5008  alephval2 5052  cflim 5059  squeeze0 6069  nnleltp1 6100  lbreu 6213  xrub 6248  dfuzi 6373  uzwo5OLD 6382  zindd 6386  uzwo3lem2 6389  zmax 6392  zbtwnre 6393  fzrevral 6650  fsequb 6654  recan 7108  caubndi 7129  faclbnd4lem4 7154  bccl2 7174  clm4lei 7284  clmi1i 7289  2climnn 7305  2climnn0 7306  climshfti 7307  iserzshft2i 7310  climaddlem3 7319  climmullem8 7330  climubii 7356  climcaui 7359  caucvglem2 7361  caucvgi 7366  serzf0i 7372  cvgratlem1ALT 7452  cvgratlem1 7455  cvgratlem4 7458  ivthlem6 7491  ivthlem7 7492  dsupivthlem 7496  unbenlem 7716  basgen2 7851  clsval2 7895  metcnp 8098  lmle 8171  metelcls 8176  metcnp4 8181  metcn4i 8183  bcthlem2 8211  bcthlem16 8225  bcthlem17 8226  bcthlem33 8242  isgrp 8254  ringideu 8387  vacnlem3 8584  blocnilem 8719  ip2eqi 8773  minveclem27 8831  spwmo 8918  hial0 9244  hial02 9245  hial2eq 9248  hlimuniii 9384  ocorth 9440  occllem5 9453  projlem22 9483  projlem26 9487  h1de2i 9752  pjjsi 9923  lnopunilem1 10214  lnophmlem1 10220  nmcopexlem6 10235  nmcfnexlem6 10264  nlelchi 10273  riesz4i 10275  hmopidmchi 10359  stge0 10432  stle1 10433  mdi 10503  mdbr3 10505  mdbr4 10506  dmdi 10510  dmdbr3 10513  dmdbr4 10514  dmdi4 10515  mdslmd1i 10537  atss 10554  atom1d 10561  atmd 10608  sumdmdlem2 10628  cdj1i 10642  cdj3i 10650  ghomgrpilem1 10670  ghomf1olem 10681  opidon 10898  rngmgmbs4 10945  ununr 10955  osneisi 11018  cmphmp 11027  homcard 11045  cnfilca 11088  ordiso 11426  omsubindss 11449  omsubinit 11451  cnpnei 11472  cncls 11473  cnntr 11474  cnsubsp2 11484  compcov 11486  uncomp 11490  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  alexsublem3 11498  alexsublem4 11499  alexsub 11500  1stcclb 11532  2ndcctbss 11539  fnessex 11545  comppfsc 11578  neibastop2lem2 11581  fnemeet1 11589  fnemeet2 11590  fnejoin2 11592  ist1-2 11603  ist1-3 11604  fbfgss 11640  isufil2 11650  filssufil 11656  flimopn 11679  limfilcf 11683  cnpfillim 11686  flimfneii 11712  filclus 11717  fclusnei 11719  fclusbas 11722  fcluscf 11724  flimfnfcls 11727  fcluscnplem 11729  fcluscnp 11730  fcluscomp 11733  ufcomp 11734  isfclusf 11737  fclusfnei 11738  raleqfn 11790  fimax 11837  fixp 11840  inficl 11849  sdclem1 11875  sdclem2 11876  sdc 11877  seqpo 11878  incsequz 11879  metsstop 11909  mettrifi 11912  geomcau 11914  caushft 11916  hmeoopn 11960  haustlmu 11967  lmtlm 11969  sstotbnd 11992  totbndss 11993  totbndbnd 12000  heiborlem1 12011  heiborlem10 12020  heiborlem13 12023  heiborlem16 12026  heiborlem23 12033  heiborlem30 12040  heiborlem35 12045  heiborlem36 12046  rrndstprj2 12074  rrncms 12075  phtpycom 12092  phtpyco 12098

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-ral 1695  df-v 1858

Copyright terms: Public domain