Theorem

Let A and x be objects. Assume x∈UA. Let φ be a proposition. Assume for all B x∈B implies B∈A implies φ. Then we have φ.

Background

The following background is necessary to understand this theorem.

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

(.) Let A be an object. Then UA is an object.

Background for Proof

The following background is necessary for the proof.

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

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

(.) Let φ(x) be a proposition depending on an object x. Then ∀x φ(x) is a proposition.

(.) Let φ(x) be a proposition depending on an object x. Then ∃x φ(x) is a proposition.

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

(.) Let φ(x) be a proposition depending on an object x. Assume ∀x φ(x). Let x be an object. Then we know φ(x).

(.) We know ∀A ∀x (x∈UA≡∃B (x∈B∧B∈A)).

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

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

(.) Let φ(x) be a proposition depending on an object x. Assume ∃x φ(x). Let ψ be a proposition. Assume for all x φ(x) implies ψ. Then we know ψ.

Proof

Claim: ∃B (x∈B∧B∈A).

Proof of Claim: Using x∈UA, it is enough to show x∈UA≡∃B (x∈B∧B∈A). We will show ∀x (x∈UA≡∃B (x∈B∧B∈A)). We have ∀A ∀x (x∈UA≡∃B (x∈B∧B∈A)). Using this, we are done. This completes the proof of the claim.

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

Hide Background.

Test yourself on this item.