Theorem alral 2153

Description: Universal quantification implies restricted quantification.

Assertion

Ref	Expression
alral	|- (A.xph -> A.x e. A ph)

Proof of Theorem alral

Step	Hyp	Ref	Expression
1		ax-1 4	. . 3 |- (ph -> (x e. A -> ph))
2	1	alimi 1338	. 2 |- (A.xph -> A.x(x e. A -> ph))
3		df-ral 2109	. 2 |- (A.x e. A ph <-> A.x(x e. A -> ph))
4	2, 3	sylibr 217	1 |- (A.xph -> A.x e. A ph)

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

This theorem is referenced by:  truni 3425  find 3977  asymref2 4310  brdom5 5964  brdom4 5965  bnj165 12493  bnj166 12494  bnj225 12514  bnj227 12515  bnj72 13208  bnj98 13221  truniOLD 13792  elpotr 13847  fincmpzer 14711  ordelordaxrVD 16691

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

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

Copyright terms: Public domain