Theorem intmin2 2611

Description: Any set is the smallest of all sets that include it.

Hypothesis

Ref	Expression
intmin2.1	|- A e. V

Assertion

Ref	Expression
intmin2	|- |^|{x | A (_ x} = A

Distinct variable group:   x,A

Proof of Theorem intmin2

Step	Hyp	Ref	Expression
1		rabab 1869	. . 3 |- {x e. V | A (_ x} = {x | A (_ x}
2	1	inteqi 2591	. 2 |- |^|{x e. V | A (_ x} = |^|{x | A (_ x}
3		intmin2.1	. . 3 |- A e. V
4		intmin 2607	. . 3 |- (A e. V -> |^|{x e. V | A (_ x} = A)
5	3, 4	ax-mp 7	. 2 |- |^|{x e. V | A (_ x} = A
6	2, 5	eqtr3i 1544	1 |- |^|{x | A (_ x} = A

Syntax hints:   = wceq 997   e. wcel 999  {cab 1509  {crab 1695  Vcvv 1858   (_ wss 2098  |^|cint 2587

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-12 1009  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022  df-sb 1214  df-clab 1510  df-cleq 1515  df-clel 1518  df-ral 1696  df-rab 1699  df-v 1859  df-in 2102  df-ss 2104  df-int 2588

Copyright terms: Public domain