Theorem ra4 1741

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 1696	. 2 |- (A.x e. A ph <-> A.x(x e. A -> ph))
2		ax-4 1014	. 2 |- (A.x(x e. A -> ph) -> (x e. A -> ph))
3	1, 2	sylbi 206	1 |- (A.x e. A ph -> (x e. A -> ph))

Syntax hints:   -> wi 3  A.wal 995   e. wcel 999  A.wral 1692

This theorem is referenced by:  ra42 1743  rspec 1744  r19.12 1787  r19.15 1800  uniiunlem 2183  ss2iun 2631  iineq2 2633  dfiun2g 2640  trss 2744  ralxfrd 2954  ralxfr 2956  peano5 3210  fnopabg 3672  elrnopabg 3857  chfnrn 3859  fopab2 3880  ffnfv 3885  iunon 3967  iinon 3968  tfrlem1 3969  tfrlem9 3977  tfr3 3984  tz7.48-1 4014  tz7.49 4017  nneneq 4577  r1tr 4716  scottex 4778  aceq6b 4804  bccl2 7061  sumeq2 7075  clm4lei 7171  clm0i 7173  clm0nnsi 7175  climabs0i 7203  climsupi 7245  caucvglem6 7252  tgcl 7713  ringid 8229  ubthlem10 8622  ubthlem11 8623  nmcopexlem1 10034  nmcfnexlem1 10063  nlelchi 10077  cnlnadjlem5 10087  rnbra 10123  homcard 10633  cmpmon 10825  hgrablkne0 10857  hgrablkcard 10858

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

This theorem depends on definitions:  df-bi 154  df-ral 1696

Copyright terms: Public domain