Theorem ra4 1694

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 1649	. 2 |- (A.x e. A ph <-> A.x(x e. A -> ph))
2		ax-4 973	. 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 954   e. wcel 958  A.wral 1645

This theorem is referenced by:  ra42 1696  rspec 1697  r19.12 1740  r19.15 1753  uniiunlem 2132  ss2iun 2577  iineq2 2579  dfiun2g 2586  trss 2689  ralxfrd 2897  ralxfr 2899  peano5 3153  fnopabg 3615  elrnopabg 3800  chfnrn 3802  fopab2 3823  ffnfv 3828  iunon 3909  iinon 3910  tfrlem1 3911  tfrlem9 3919  tfr3 3926  tz7.48-1 3956  tz7.49 3959  nneneq 4512  r1tr 4654  scottex 4716  aceq6b 4742  bccl2t 6971  sumeq2 6985  clm4le 7081  clm0 7083  clm0nns 7085  climabs0 7113  climsup 7155  caucvglem6 7162  tgclt 7624  ringid 8145  ubthlem10 8538  ubthlem11 8539  nmcopexlem1 9951  nmcfnexlem1 9980  nlelch 9994  cnlnadjlem5 10004  rnbra 10040  homcard 10539  cmpmon 10743  hgrablkne0 10773  hgrablkcard 10774

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

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

Copyright terms: Public domain