Satallax
Satallax is a higher-order
automated theorem prover.
Satallax won the THF division
of CASC-23 in 2011.

Matracas Mathematics Related Software

Impressum
Contact Person
Chad E Brown

Theorem

Let A and B be objects. Assume A \ B=∅. Then we have AB.

Background

The following background is necessary to understand this theorem.

(.) Let x and y be objects. Then x=y is a proposition.

(.) ∅ is an object.

(.) Let A and B be objects. Then "AB" is a proposition.

(.) Let A and B be objects. Then "A \ B" is an object.

Background for Proof

The following background is necessary for the proof.

(.) Let A and x be objects. Then xA is a proposition.

(.) Let φ be a proposition. Then ¬φ is a proposition.

(.) Let φ and ψ be propositions. Then φψ is a proposition.

(.) Let φ and ψ be propositions. Assume φψ and φ. Then we know ψ.

(.) "false" is a proposition.

(.) Let x be an object. Assume x∈∅. Let φ be a proposition. Then we know φ.

(.) Let φ be a proposition. Assume ¬φ implies false. Then we know φ.

(.) Let x be an object. Then we know x=x.

(.) Let A and B be objects. Assume A=B. Let x and y be objects. Assume x=y. Then we know xAyB.

(.) Let A and B be objects. Assume for all x xA implies xB. Then we know AB.

(.) Let A, B and x be objects. Assume xA and ¬xB. Then we know xA \ B.

Proof

It is enough to show for all x xA implies xB. Let x be an object. Assume xA. We will show ¬xB implies false. Assume ¬xB. It is enough to show x∈∅. Since A \ B=∅, we know xA \ Bx∈∅. Since ¬xB and xA, we have xA \ B. Using this and xA \ Bx∈∅, we are done.


Click here to modify variable names (JavaScript Must Be Enabled).

Hide Background.

Test yourself on this item.