Theorem ra4 1697

Description: Restricted specialization.

Assertion

Ref	Expression
ra4	|- (A.x e. A ph -> (x e. A -> ph))

Proof of Theorem ra4

Step	Hyp	Ref	Expression
1		df-ral 1652	. 2 |- (A.x e. A ph <-> A.x(x e. A -> ph))
2		ax-4 975	. 2 |- (A.x(x e. A -> ph) -> (x e. A -> ph))
3	1, 2	sylbi 199	1 |- (A.x e. A ph -> (x e. A -> ph))

Syntax hints:   -> wi 3  A.wal 956   e. wcel 960  A.wral 1648

This theorem is referenced by:  ra42 1699  rspec 1700  r19.12 1743  r19.15 1756  uniiunlem 2136  ss2iun 2582  iineq2 2584  dfiun2g 2591  trss 2695  ralxfrd 2904  ralxfr 2906  peano5 3160  fnopabg 3622  elrnopabg 3807  chfnrn 3809  fopab2 3830  ffnfv 3835  iunon 3916  iinon 3917  tfrlem1 3918  tfrlem9 3926  tfr3 3933  tz7.48-1 3963  tz7.49 3966  nneneq 4519  r1tr 4671  scottex 4733  aceq6b 4759  bccl2t 6978  sumeq2 6992  clm4le 7088  clm0 7090  clm0nns 7092  climabs0 7120  climsup 7162  caucvglem6 7169  tgclt 7630  ringid 8148  ubthlem10 8541  ubthlem11 8542  nmcopexlem1 9953  nmcfnexlem1 9982  nlelch 9996  cnlnadjlem5 10006  rnbra 10042  homcard 10533  cmpmon 10722  hgrablkne0 10752  hgrablkcard 10753

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 975

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

Copyright terms: Public domain