Theorem ra4 1691

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 1646	. 2 |- (A.x e. A ph <-> A.x(x e. A -> ph))
2		ax-4 971	. 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 952   e. wcel 956  A.wral 1642

This theorem is referenced by:  ra42 1693  rspec 1694  r19.12 1737  r19.15 1750  uniiunlem 2128  ss2iun 2572  iineq2 2574  dfiun2g 2581  trss 2684  ralxfrd 2892  ralxfr 2894  peano5 3148  fnopabg 3607  elrnopabg 3791  chfnrn 3793  fopab2 3814  ffnfv 3819  iunon 3900  iinon 3901  tfrlem1 3902  tfrlem9 3910  tfr3 3917  tz7.48-1 3947  tz7.49 3950  nneneq 4498  r1tr 4634  scottex 4696  aceq6b 4722  bccl2t 6917  sumeq2 6931  clm4le 7027  clm0 7029  clm0nns 7031  climsup 7099  caucvglem6 7106  tgclt 7574  ringid 8097  ubthlem10 8482  ubthlem11 8483  nmcopexlem1 9889  nmcfnexlem1 9918  nlelch 9932  cnlnadjlem5 9942  rnbra 9978  homcard 10462  cmpmon 10621  hgrablkne0 10645  hgrablkcard 10646

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

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

Copyright terms: Public domain