Theorem ra4 1740

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 1695	. 2 |- (A.x e. A ph <-> A.x(x e. A -> ph))
2		ax-4 1009	. 2 |- (A.x(x e. A -> ph) -> (x e. A -> ph))
3	1, 2	sylbi 197	1 |- (A.x e. A ph -> (x e. A -> ph))

Syntax hints:   -> wi 3  A.wal 990   e. wcel 994  A.wral 1691

This theorem is referenced by:  ra42 1742  rspec 1743  r19.12 1786  r19.15 1799  uniiunlem 2184  ss2iun 2645  iineq2 2647  dfiun2g 2654  trss 2763  ralxfrd 3120  ralxfr 3122  peano5 3241  fnopabg 3722  elrnopabg 3914  chfnrn 3916  fopab2 3937  ffnfv 3942  iunon 4207  iinon 4208  onopriun 4211  tfrlem1 4212  tfrlem9 4220  tfr3 4227  tz7.48-1 4257  tz7.49 4260  ac6sfilem3 4590  nneneq 4659  r1tr 4800  scottex 4862  aceq6b 4888  bccl2 7174  sumeq2 7188  clm4lei 7284  clm0i 7286  clm0nnsi 7288  climabs0i 7316  climsupi 7358  caucvglem6 7365  tgcl 7836  metequiv 8091  ringid 8386  ubthlem10 8796  ubthlem11 8797  nmcopexlem1 10230  nmcfnexlem1 10259  nlelchi 10273  cnlnadjlem5 10283  rnbra 10320  imgfldref2 10768  tostos 10883  homcard 11045  cmpmon 11270  ordtypelem6 11432  ordtypelem7 11433  omsubsdomlem2 11441  elomsubsd 11446  hscptsscld 11491  alexsublem3 11498  topbasfne 11560  neibastop1 11579  neibastop2lem3 11582  neibastop2 11584  neibastop3 11585  limfilcf 11683  gafo 11773  gagrpid 11780  gaass 11781  indexd 11846  indexf 11847  filbcmb 11857  hgrablkne0 12199  hgrablkcard 12200

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

This theorem depends on definitions:  df-bi 145  df-ral 1695

Copyright terms: Public domain