Theorem ra4 2155

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 2109	. 2 |- (A.x e. A ph <-> A.x(x e. A -> ph))
2		ax-4 1319	. 2 |- (A.x(x e. A -> ph) -> (x e. A -> ph))
3	1, 2	sylbi 216	1 |- (A.x e. A ph -> (x e. A -> ph))

Syntax hints:   -> wi 3  A.wal 1296   e. wcel 1300  A.wral 2105

This theorem is referenced by:  ra42 2157  rspec 2158  r19.12 2204  r19.12OLD 2205  ralbi 2223  uniiunlem 2693  ss2iunOLD 3272  iineq2OLD 3275  dfiun2g 3283  dfiun2gOLD 3284  trss 3421  eufromeq1 3828  eufromeq5 3832  ralxfrd 3837  ralxfr 3839  peano5 3975  asymref2 4310  fnopabg 4546  elrnopabg 4773  chfnrn 4775  fopab2 4796  ffnfv 4801  iunon 5114  iinon 5115  onopriun 5118  tfrlem1 5119  tfrlem9 5127  tfr3 5134  tz7.48-1 5165  tz7.49 5168  ac6sfilem3 5508  nneneq 5606  ordtypelem6 5689  ordtypelem7 5690  r1tr 5765  scottex 5846  omsubsdomlem2 5880  elomsubsd 5885  aceq6b 5904  bccl2 8223  sumeq2 8245  clm4lei 8341  clm0i 8343  clm0nnsi 8345  climabs0i 8373  climsupi 8415  caucvglem6 8422  tgcl 8894  metequiv 9158  gafo 9451  gagrpid 9458  gaass 9459  ringid 9469  ubthlem10 9881  ubthlem11 9882  indexfi 10174  nmcopexlem1 11588  nmcfnexlem1 11617  nlelchi 11631  cnlnadjlem5 11641  rnbra 11678  bnj10 12374  bnj180 12497  bnj228 12517  bnj1439 13133  bnj590 13298  bnj594 13300  bnj1128 13428  r19.21 13818  dfon2lem3 13851  dfon2lem7 13855  wfrlem4 13960  wfrlem12 13968  frr3g 13980  imgfldref2 14368  fopab2g 14485  tostos 14637  prodeq2 14661  fnopabco2b 14734  curgrpact 14735  homcard 14893  cmpmon 15164  ordtypelem6OLD 15380  ordtypelem7OLD 15381  omsubsdomlem2OLD 15389  elomsubsdOLD 15394  hscptsscld 15434  alexsublem3 15439  topbasfne 15499  neibastop1 15518  neibastop2lem3 15521  neibastop2 15523  neibastop3 15524  limfilcf 15587  cover2 15673  indexdom 15754  indexfiOLD 15755  filbcmb 15776  hgrablkne0 16295  hgrablkcard 16296  trintALTVD 16704  trintALT 16705  glbconx 17029  pmapglbx 17251  pmapglb2x 17254

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

This theorem depends on definitions:  df-bi 164  df-ral 2109

Copyright terms: Public domain