Home | Metamath
Proof Explorer Theorem List (p. 46 of 466) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29289) |
Hilbert Space Explorer
(29290-30812) |
Users' Mathboxes
(30813-46532) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eqif 4501 | Expansion of an equality with a conditional operator. (Contributed by NM, 14-Feb-2005.) |
⊢ (𝐴 = if(𝜑, 𝐵, 𝐶) ↔ ((𝜑 ∧ 𝐴 = 𝐵) ∨ (¬ 𝜑 ∧ 𝐴 = 𝐶))) | ||
Theorem | ifval 4502 | Another expression of the value of the if predicate, analogous to eqif 4501. See also the more specialized iftrue 4466 and iffalse 4469. (Contributed by BJ, 6-Apr-2019.) |
⊢ (𝐴 = if(𝜑, 𝐵, 𝐶) ↔ ((𝜑 → 𝐴 = 𝐵) ∧ (¬ 𝜑 → 𝐴 = 𝐶))) | ||
Theorem | elif 4503 | Membership in a conditional operator. (Contributed by NM, 14-Feb-2005.) |
⊢ (𝐴 ∈ if(𝜑, 𝐵, 𝐶) ↔ ((𝜑 ∧ 𝐴 ∈ 𝐵) ∨ (¬ 𝜑 ∧ 𝐴 ∈ 𝐶))) | ||
Theorem | ifel 4504 | Membership of a conditional operator. (Contributed by NM, 10-Sep-2005.) |
⊢ (if(𝜑, 𝐴, 𝐵) ∈ 𝐶 ↔ ((𝜑 ∧ 𝐴 ∈ 𝐶) ∨ (¬ 𝜑 ∧ 𝐵 ∈ 𝐶))) | ||
Theorem | ifcl 4505 | Membership (closure) of a conditional operator. (Contributed by NM, 4-Apr-2005.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶) | ||
Theorem | ifcld 4506 | Membership (closure) of a conditional operator, deduction form. (Contributed by SO, 16-Jul-2018.) |
⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶) | ||
Theorem | ifcli 4507 | Inference associated with ifcl 4505. Membership (closure) of a conditional operator. Also usable to keep a membership hypothesis for the weak deduction theorem dedth 4518 when the special case 𝐵 ∈ 𝐶 is provable. (Contributed by NM, 14-Aug-1999.) (Proof shortened by BJ, 1-Sep-2022.) |
⊢ 𝐴 ∈ 𝐶 & ⊢ 𝐵 ∈ 𝐶 ⇒ ⊢ if(𝜑, 𝐴, 𝐵) ∈ 𝐶 | ||
Theorem | ifexd 4508 | Existence of the conditional operator (deduction form). (Contributed by SN, 26-Jul-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ V) | ||
Theorem | ifexg 4509 | Existence of the conditional operator (closed form). (Contributed by NM, 21-Mar-2011.) (Proof shortened by BJ, 1-Sep-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → if(𝜑, 𝐴, 𝐵) ∈ V) | ||
Theorem | ifex 4510 | Existence of the conditional operator (inference form). (Contributed by NM, 2-Sep-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ if(𝜑, 𝐴, 𝐵) ∈ V | ||
Theorem | ifeqor 4511 | The possible values of a conditional operator. (Contributed by NM, 17-Jun-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (if(𝜑, 𝐴, 𝐵) = 𝐴 ∨ if(𝜑, 𝐴, 𝐵) = 𝐵) | ||
Theorem | ifnot 4512 | Negating the first argument swaps the last two arguments of a conditional operator. (Contributed by NM, 21-Jun-2007.) |
⊢ if(¬ 𝜑, 𝐴, 𝐵) = if(𝜑, 𝐵, 𝐴) | ||
Theorem | ifan 4513 | Rewrite a conjunction in a conditional as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) | ||
Theorem | ifor 4514 | Rewrite a disjunction in a conditional as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ if((𝜑 ∨ 𝜓), 𝐴, 𝐵) = if(𝜑, 𝐴, if(𝜓, 𝐴, 𝐵)) | ||
Theorem | 2if2 4515 | Resolve two nested conditionals. (Contributed by Alexander van der Vekens, 27-Mar-2018.) |
⊢ ((𝜑 ∧ 𝜓) → 𝐷 = 𝐴) & ⊢ ((𝜑 ∧ ¬ 𝜓 ∧ 𝜃) → 𝐷 = 𝐵) & ⊢ ((𝜑 ∧ ¬ 𝜓 ∧ ¬ 𝜃) → 𝐷 = 𝐶) ⇒ ⊢ (𝜑 → 𝐷 = if(𝜓, 𝐴, if(𝜃, 𝐵, 𝐶))) | ||
Theorem | ifcomnan 4516 | Commute the conditions in two nested conditionals if both conditions are not simultaneously true. (Contributed by SO, 15-Jul-2018.) |
⊢ (¬ (𝜑 ∧ 𝜓) → if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = if(𝜓, 𝐵, if(𝜑, 𝐴, 𝐶))) | ||
Theorem | csbif 4517 | Distribute proper substitution through the conditional operator. (Contributed by NM, 24-Feb-2013.) (Revised by NM, 19-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌if(𝜑, 𝐵, 𝐶) = if([𝐴 / 𝑥]𝜑, ⦋𝐴 / 𝑥⦌𝐵, ⦋𝐴 / 𝑥⦌𝐶) | ||
This subsection contains a few results related to the weak deduction theorem in set theory. For the weak deduction theorem in propositional calculus, see the section beginning with elimh 1082. For more information on the weak deduction theorem, see the Weak Deduction Theorem page mmdeduction.html 1082. In a Hilbert system of logic (which consists of a set of axioms, modus ponens, and the generalization rule), converting a deduction to a proof using the Deduction Theorem (taught in introductory logic books) involves an exponential increase of the number of steps as hypotheses are successively eliminated. Here is a trick that is not as general as the Deduction Theorem but requires only a linear increase in the number of steps. The general problem: We want to convert a deduction P |- Q into a proof of the theorem |- P -> Q i.e., we want to eliminate the hypothesis P. Normally this is done using the Deduction (meta)Theorem, which looks at the microscopic steps of the deduction and usually doubles or triples the number of these microscopic steps for each hypothesis that is eliminated. We will look at a special case of this problem, without appealing to the Deduction Theorem. We assume ZF with class notation. A and B are arbitrary (possibly proper) classes. P, Q, R, S and T are wffs. We define the conditional operator, if(P, A, B), as follows: if(P, A, B) =def= { x | (x \in A & P) v (x \in B & -. P) } (where x does not occur in A, B, or P). Lemma 1. A = if(P, A, B) -> (P <-> R), B = if(P, A, B) -> (S <-> R), S |- R Proof: Logic and Axiom of Extensionality. Lemma 2. A = if(P, A, B) -> (Q <-> T), T |- P -> Q Proof: Logic and Axiom of Extensionality. Here is a simple example that illustrates how it works. Suppose we have a deduction Ord A |- Tr A which means, "Assume A is an ordinal class. Then A is a transitive class." Note that A is a class variable that may be substituted with any class expression, so this is really a deduction scheme. We want to convert this to a proof of the theorem (scheme) |- Ord A -> Tr A. The catch is that we must be able to prove "Ord A" for at least one object A (and this is what makes it weaker than the ordinary Deduction Theorem). However, it is easy to prove |- Ord 0 (the empty set is ordinal). (For a typical textbook "theorem", i.e., deduction, there is usually at least one object satisfying each hypothesis, otherwise the theorem would not be very useful. We can always go back to the standard Deduction Theorem for those hypotheses where this is not the case.) Continuing with the example: Equality axioms (and Extensionality) yield |- A = if(Ord A, A, 0) -> (Ord A <-> Ord if(Ord A, A, 0)) (1) |- 0 = if(Ord A, A, 0) -> (Ord 0 <-> Ord if(Ord A, A, 0)) (2) From (1), (2) and |- Ord 0, Lemma 1 yields |- Ord if(Ord A, A, 0) (3) From (3) and substituting if(Ord A, A, 0) for A in the original deduction, |- Tr if(Ord A, A, 0) (4) Equality axioms (and Extensionality) yield |- A = if(Ord A, A, 0) -> (Tr A <-> Tr if(Ord A, A, 0)) (5) From (4) and (5), Lemma 2 yields |- Ord A -> Tr A (Q.E.D.) | ||
Theorem | dedth 4518 | Weak deduction theorem that eliminates a hypothesis 𝜑, making it become an antecedent. We assume that a proof exists for 𝜑 when the class variable 𝐴 is replaced with a specific class 𝐵. The hypothesis 𝜒 should be assigned to the inference, and the inference hypothesis eliminated with elimhyp 4525. If the inference has other hypotheses with class variable 𝐴, these can be kept by assigning keephyp 4531 to them. For more information, see the Weak Deduction Theorem page mmdeduction.html 4531. (Contributed by NM, 15-May-1999.) |
⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜒)) & ⊢ 𝜒 ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | dedth2h 4519 | Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v 4522 but requires that each hypothesis have exactly one class variable. See also comments in dedth 4518. (Contributed by NM, 15-May-1999.) |
⊢ (𝐴 = if(𝜑, 𝐴, 𝐶) → (𝜒 ↔ 𝜃)) & ⊢ (𝐵 = if(𝜓, 𝐵, 𝐷) → (𝜃 ↔ 𝜏)) & ⊢ 𝜏 ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | dedth3h 4520 | Weak deduction theorem eliminating three hypotheses. See comments in dedth2h 4519. (Contributed by NM, 15-May-1999.) |
⊢ (𝐴 = if(𝜑, 𝐴, 𝐷) → (𝜃 ↔ 𝜏)) & ⊢ (𝐵 = if(𝜓, 𝐵, 𝑅) → (𝜏 ↔ 𝜂)) & ⊢ (𝐶 = if(𝜒, 𝐶, 𝑆) → (𝜂 ↔ 𝜁)) & ⊢ 𝜁 ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | dedth4h 4521 | Weak deduction theorem eliminating four hypotheses. See comments in dedth2h 4519. (Contributed by NM, 16-May-1999.) |
⊢ (𝐴 = if(𝜑, 𝐴, 𝑅) → (𝜏 ↔ 𝜂)) & ⊢ (𝐵 = if(𝜓, 𝐵, 𝑆) → (𝜂 ↔ 𝜁)) & ⊢ (𝐶 = if(𝜒, 𝐶, 𝐹) → (𝜁 ↔ 𝜎)) & ⊢ (𝐷 = if(𝜃, 𝐷, 𝐺) → (𝜎 ↔ 𝜌)) & ⊢ 𝜌 ⇒ ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) | ||
Theorem | dedth2v 4522 | Weak deduction theorem for eliminating a hypothesis with 2 class variables. Note: if the hypothesis can be separated into two hypotheses, each with one class variable, then dedth2h 4519 is simpler to use. See also comments in dedth 4518. (Contributed by NM, 13-Aug-1999.) (Proof shortened by Eric Schmidt, 28-Jul-2009.) |
⊢ (𝐴 = if(𝜑, 𝐴, 𝐶) → (𝜓 ↔ 𝜒)) & ⊢ (𝐵 = if(𝜑, 𝐵, 𝐷) → (𝜒 ↔ 𝜃)) & ⊢ 𝜃 ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | dedth3v 4523 | Weak deduction theorem for eliminating a hypothesis with 3 class variables. See comments in dedth2v 4522. (Contributed by NM, 13-Aug-1999.) (Proof shortened by Eric Schmidt, 28-Jul-2009.) |
⊢ (𝐴 = if(𝜑, 𝐴, 𝐷) → (𝜓 ↔ 𝜒)) & ⊢ (𝐵 = if(𝜑, 𝐵, 𝑅) → (𝜒 ↔ 𝜃)) & ⊢ (𝐶 = if(𝜑, 𝐶, 𝑆) → (𝜃 ↔ 𝜏)) & ⊢ 𝜏 ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | dedth4v 4524 | Weak deduction theorem for eliminating a hypothesis with 4 class variables. See comments in dedth2v 4522. (Contributed by NM, 21-Apr-2007.) (Proof shortened by Eric Schmidt, 28-Jul-2009.) |
⊢ (𝐴 = if(𝜑, 𝐴, 𝑅) → (𝜓 ↔ 𝜒)) & ⊢ (𝐵 = if(𝜑, 𝐵, 𝑆) → (𝜒 ↔ 𝜃)) & ⊢ (𝐶 = if(𝜑, 𝐶, 𝑇) → (𝜃 ↔ 𝜏)) & ⊢ (𝐷 = if(𝜑, 𝐷, 𝑈) → (𝜏 ↔ 𝜂)) & ⊢ 𝜂 ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | elimhyp 4525 | Eliminate a hypothesis containing class variable 𝐴 when it is known for a specific class 𝐵. For more information, see comments in dedth 4518. (Contributed by NM, 15-May-1999.) |
⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜑 ↔ 𝜓)) & ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜓)) & ⊢ 𝜒 ⇒ ⊢ 𝜓 | ||
Theorem | elimhyp2v 4526 | Eliminate a hypothesis containing 2 class variables. (Contributed by NM, 14-Aug-1999.) |
⊢ (𝐴 = if(𝜑, 𝐴, 𝐶) → (𝜑 ↔ 𝜒)) & ⊢ (𝐵 = if(𝜑, 𝐵, 𝐷) → (𝜒 ↔ 𝜃)) & ⊢ (𝐶 = if(𝜑, 𝐴, 𝐶) → (𝜏 ↔ 𝜂)) & ⊢ (𝐷 = if(𝜑, 𝐵, 𝐷) → (𝜂 ↔ 𝜃)) & ⊢ 𝜏 ⇒ ⊢ 𝜃 | ||
Theorem | elimhyp3v 4527 | Eliminate a hypothesis containing 3 class variables. (Contributed by NM, 14-Aug-1999.) |
⊢ (𝐴 = if(𝜑, 𝐴, 𝐷) → (𝜑 ↔ 𝜒)) & ⊢ (𝐵 = if(𝜑, 𝐵, 𝑅) → (𝜒 ↔ 𝜃)) & ⊢ (𝐶 = if(𝜑, 𝐶, 𝑆) → (𝜃 ↔ 𝜏)) & ⊢ (𝐷 = if(𝜑, 𝐴, 𝐷) → (𝜂 ↔ 𝜁)) & ⊢ (𝑅 = if(𝜑, 𝐵, 𝑅) → (𝜁 ↔ 𝜎)) & ⊢ (𝑆 = if(𝜑, 𝐶, 𝑆) → (𝜎 ↔ 𝜏)) & ⊢ 𝜂 ⇒ ⊢ 𝜏 | ||
Theorem | elimhyp4v 4528 | Eliminate a hypothesis containing 4 class variables (for use with the weak deduction theorem dedth 4518). (Contributed by NM, 16-Apr-2005.) |
⊢ (𝐴 = if(𝜑, 𝐴, 𝐷) → (𝜑 ↔ 𝜒)) & ⊢ (𝐵 = if(𝜑, 𝐵, 𝑅) → (𝜒 ↔ 𝜃)) & ⊢ (𝐶 = if(𝜑, 𝐶, 𝑆) → (𝜃 ↔ 𝜏)) & ⊢ (𝐹 = if(𝜑, 𝐹, 𝐺) → (𝜏 ↔ 𝜓)) & ⊢ (𝐷 = if(𝜑, 𝐴, 𝐷) → (𝜂 ↔ 𝜁)) & ⊢ (𝑅 = if(𝜑, 𝐵, 𝑅) → (𝜁 ↔ 𝜎)) & ⊢ (𝑆 = if(𝜑, 𝐶, 𝑆) → (𝜎 ↔ 𝜌)) & ⊢ (𝐺 = if(𝜑, 𝐹, 𝐺) → (𝜌 ↔ 𝜓)) & ⊢ 𝜂 ⇒ ⊢ 𝜓 | ||
Theorem | elimel 4529 | Eliminate a membership hypothesis for weak deduction theorem, when special case 𝐵 ∈ 𝐶 is provable. (Contributed by NM, 15-May-1999.) |
⊢ 𝐵 ∈ 𝐶 ⇒ ⊢ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶 | ||
Theorem | elimdhyp 4530 | Version of elimhyp 4525 where the hypothesis is deduced from the final antecedent. See divalg 16121 for an example of its use. (Contributed by Paul Chapman, 25-Mar-2008.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜒)) & ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜃 ↔ 𝜒)) & ⊢ 𝜃 ⇒ ⊢ 𝜒 | ||
Theorem | keephyp 4531 | Transform a hypothesis 𝜓 that we want to keep (but contains the same class variable 𝐴 used in the eliminated hypothesis) for use with the weak deduction theorem. (Contributed by NM, 15-May-1999.) |
⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃)) & ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃)) & ⊢ 𝜓 & ⊢ 𝜒 ⇒ ⊢ 𝜃 | ||
Theorem | keephyp2v 4532 | Keep a hypothesis containing 2 class variables (for use with the weak deduction theorem dedth 4518). (Contributed by NM, 16-Apr-2005.) |
⊢ (𝐴 = if(𝜑, 𝐴, 𝐶) → (𝜓 ↔ 𝜒)) & ⊢ (𝐵 = if(𝜑, 𝐵, 𝐷) → (𝜒 ↔ 𝜃)) & ⊢ (𝐶 = if(𝜑, 𝐴, 𝐶) → (𝜏 ↔ 𝜂)) & ⊢ (𝐷 = if(𝜑, 𝐵, 𝐷) → (𝜂 ↔ 𝜃)) & ⊢ 𝜓 & ⊢ 𝜏 ⇒ ⊢ 𝜃 | ||
Theorem | keephyp3v 4533 | Keep a hypothesis containing 3 class variables. (Contributed by NM, 27-Sep-1999.) |
⊢ (𝐴 = if(𝜑, 𝐴, 𝐷) → (𝜌 ↔ 𝜒)) & ⊢ (𝐵 = if(𝜑, 𝐵, 𝑅) → (𝜒 ↔ 𝜃)) & ⊢ (𝐶 = if(𝜑, 𝐶, 𝑆) → (𝜃 ↔ 𝜏)) & ⊢ (𝐷 = if(𝜑, 𝐴, 𝐷) → (𝜂 ↔ 𝜁)) & ⊢ (𝑅 = if(𝜑, 𝐵, 𝑅) → (𝜁 ↔ 𝜎)) & ⊢ (𝑆 = if(𝜑, 𝐶, 𝑆) → (𝜎 ↔ 𝜏)) & ⊢ 𝜌 & ⊢ 𝜂 ⇒ ⊢ 𝜏 | ||
Syntax | cpw 4534 | Extend class notation to include power class. (The tilde in the Metamath token is meant to suggest the calligraphic font of the P.) |
class 𝒫 𝐴 | ||
Theorem | pwjust 4535* | Soundness justification theorem for df-pw 4536. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ {𝑥 ∣ 𝑥 ⊆ 𝐴} = {𝑦 ∣ 𝑦 ⊆ 𝐴} | ||
Definition | df-pw 4536* | Define power class. Definition 5.10 of [TakeutiZaring] p. 17, but we also let it apply to proper classes, i.e. those that are not members of V. When applied to a set, this produces its power set. A power set of S is the set of all subsets of S, including the empty set and S itself. For example, if 𝐴 = {3, 5, 7}, then 𝒫 𝐴 = {∅, {3}, {5}, {7}, {3, 5}, {3, 7}, {5, 7}, {3, 5, 7}} (ex-pw 28802). We will later introduce the Axiom of Power Sets ax-pow 5289, which can be expressed in class notation per pwexg 5302. Still later we will prove, in hashpw 14160, that the size of the power set of a finite set is 2 raised to the power of the size of the set. (Contributed by NM, 24-Jun-1993.) |
⊢ 𝒫 𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴} | ||
Theorem | elpwg 4537 | Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 5269. (Contributed by NM, 6-Aug-2000.) (Proof shortened by BJ, 31-Dec-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | elpw 4538 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 31-Dec-1993.) (Proof shortened by BJ, 31-Dec-2023.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) | ||
Theorem | velpw 4539 | Setvar variable membership in a power class. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) | ||
Theorem | elpwOLD 4540 | Obsolete proof of elpw 4538 as of 31-Dec-2023. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by NM, 31-Dec-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) | ||
Theorem | elpwgOLD 4541 | Obsolete proof of elpwg 4537 as of 31-Dec-2023. (Contributed by NM, 6-Aug-2000.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | elpwd 4542 | Membership in a power class. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵) | ||
Theorem | elpwi 4543 | Subset relation implied by membership in a power class. (Contributed by NM, 17-Feb-2007.) |
⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵) | ||
Theorem | elpwb 4544 | Characterization of the elements of a power class. (Contributed by BJ, 29-Apr-2021.) |
⊢ (𝐴 ∈ 𝒫 𝐵 ↔ (𝐴 ∈ V ∧ 𝐴 ⊆ 𝐵)) | ||
Theorem | elpwid 4545 | An element of a power class is a subclass. Deduction form of elpwi 4543. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | elelpwi 4546 | If 𝐴 belongs to a part of 𝐶, then 𝐴 belongs to 𝐶. (Contributed by FL, 3-Aug-2009.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝒫 𝐶) → 𝐴 ∈ 𝐶) | ||
Theorem | sspw 4547 | The powerclass preserves inclusion. See sspwb 5366 for the biconditional version. (Contributed by NM, 13-Oct-1996.) Extract forward implication of sspwb 5366 since it requires fewer axioms. (Revised by BJ, 13-Apr-2024.) |
⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵) | ||
Theorem | sspwi 4548 | The powerclass preserves inclusion (inference form). (Contributed by BJ, 13-Apr-2024.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ 𝒫 𝐴 ⊆ 𝒫 𝐵 | ||
Theorem | sspwd 4549 | The powerclass preserves inclusion (deduction form). (Contributed by BJ, 13-Apr-2024.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝒫 𝐴 ⊆ 𝒫 𝐵) | ||
Theorem | pweq 4550 | Equality theorem for power class. (Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ, 13-Apr-2024.) |
⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵) | ||
Theorem | pweqALT 4551 | Alternate proof of pweq 4550 directly from the definition. (Contributed by NM, 21-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵) | ||
Theorem | pweqi 4552 | Equality inference for power class. (Contributed by NM, 27-Nov-2013.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ 𝒫 𝐴 = 𝒫 𝐵 | ||
Theorem | pweqd 4553 | Equality deduction for power class. (Contributed by NM, 27-Nov-2013.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝒫 𝐴 = 𝒫 𝐵) | ||
Theorem | pwunss 4554 | The power class of the union of two classes includes the union of their power classes. Exercise 4.12(k) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.) Remove use of ax-sep 5224, ax-nul 5231, ax-pr 5353 and shorten proof. (Revised by BJ, 13-Apr-2024.) |
⊢ (𝒫 𝐴 ∪ 𝒫 𝐵) ⊆ 𝒫 (𝐴 ∪ 𝐵) | ||
Theorem | nfpw 4555 | Bound-variable hypothesis builder for power class. (Contributed by NM, 28-Oct-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥𝒫 𝐴 | ||
Theorem | pwidg 4556 | A set is an element of its power set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴) | ||
Theorem | pwidb 4557 | A class is an element of its powerclass if and only if it is a set. (Contributed by BJ, 31-Dec-2023.) |
⊢ (𝐴 ∈ V ↔ 𝐴 ∈ 𝒫 𝐴) | ||
Theorem | pwid 4558 | A set is a member of its power class. Theorem 87 of [Suppes] p. 47. (Contributed by NM, 5-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ 𝐴 ∈ 𝒫 𝐴 | ||
Theorem | pwss 4559* | Subclass relationship for power class. (Contributed by NM, 21-Jun-2009.) |
⊢ (𝒫 𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐵)) | ||
Theorem | pwundif 4560 | Break up the power class of a union into a union of smaller classes. (Contributed by NM, 25-Mar-2007.) (Proof shortened by Thierry Arnoux, 20-Dec-2016.) Remove use of ax-sep 5224, ax-nul 5231, ax-pr 5353 and shorten proof. (Revised by BJ, 14-Apr-2024.) |
⊢ 𝒫 (𝐴 ∪ 𝐵) = ((𝒫 (𝐴 ∪ 𝐵) ∖ 𝒫 𝐴) ∪ 𝒫 𝐴) | ||
Theorem | snjust 4561* | Soundness justification theorem for df-sn 4563. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ {𝑥 ∣ 𝑥 = 𝐴} = {𝑦 ∣ 𝑦 = 𝐴} | ||
Syntax | csn 4562 | Extend class notation to include singleton. |
class {𝐴} | ||
Definition | df-sn 4563* | Define the singleton of a class. Definition 7.1 of [Quine] p. 48. For convenience, it is well-defined for proper classes, i.e., those that are not elements of V, see snprc 4654. For an alternate definition see dfsn2 4575. (Contributed by NM, 21-Jun-1993.) |
⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} | ||
Syntax | cpr 4564 | Extend class notation to include unordered pair. |
class {𝐴, 𝐵} | ||
Definition | df-pr 4565 |
Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For
example, 𝐴 ∈ {1, -1} → (𝐴↑2) = 1 (ex-pr 28803). They are
unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 4669. For a more
traditional definition, but requiring a dummy variable, see dfpr2 4581.
{𝐴,
𝐴} is also an
unordered pair, but also a singleton because of
{𝐴} =
{𝐴, 𝐴} (see dfsn2 4575). Therefore, {𝐴, 𝐵} is called
a proper (unordered) pair iff 𝐴 ≠ 𝐵 and 𝐴 and 𝐵 are
sets.
Note: ordered pairs are a completely different object defined below in df-op 4569. When the term "pair" is used without qualifier, it generally means "unordered pair", and the context makes it clear which version is meant. (Contributed by NM, 21-Jun-1993.) |
⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) | ||
Syntax | ctp 4566 | Extend class notation to include unordered triple (sometimes called "unordered triplet"). |
class {𝐴, 𝐵, 𝐶} | ||
Definition | df-tp 4567 |
Define unordered triple of classes. Definition of [Enderton] p. 19.
Note: ordered triples are a completely different object defined below in df-ot 4571. As with all tuples, when the term "triple" is used without qualifier, it means "ordered triple". (Contributed by NM, 9-Apr-1994.) |
⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) | ||
Syntax | cop 4568 | Extend class notation to include ordered pair. |
class 〈𝐴, 𝐵〉 | ||
Definition | df-op 4569* |
Definition of an ordered pair, equivalent to Kuratowski's definition
{{𝐴}, {𝐴, 𝐵}} when the arguments are sets.
Since the
behavior of Kuratowski definition is not very useful for proper classes,
we define it to be empty in this case (see opprc1 4829, opprc2 4830, and
0nelop 5411). For Kuratowski's actual definition when
the arguments are
sets, see dfop 4804. For the justifying theorem (for sets) see
opth 5392.
See dfopif 4801 for an equivalent formulation using the if operation.
Definition 9.1 of [Quine] p. 58 defines an ordered pair unconditionally as 〈𝐴, 𝐵〉 = {{𝐴}, {𝐴, 𝐵}}, which has different behavior from our df-op 4569 when the arguments are proper classes. Ordinarily this difference is not important, since neither definition is meaningful in that case. Our df-op 4569 was chosen because it often makes proofs shorter by eliminating unnecessary sethood hypotheses. There are other ways to define ordered pairs. The basic requirement is that two ordered pairs are equal iff their respective members are equal. In 1914 Norbert Wiener gave the first successful definition 〈𝐴, 𝐵〉2 = {{{𝐴}, ∅}, {{𝐵}}}, justified by opthwiener 5429. This was simplified by Kazimierz Kuratowski in 1921 to our present definition. An even simpler definition 〈𝐴, 𝐵〉3 = {𝐴, {𝐴, 𝐵}} is justified by opthreg 9385, but it requires the Axiom of Regularity for its justification and is not commonly used. A definition that also works for proper classes is 〈𝐴, 𝐵〉4 = ((𝐴 × {∅}) ∪ (𝐵 × {{∅}})), justified by opthprc 5652. Nearly at the same time as Norbert Wiener, Felix Hausdorff proposed the following definition in "Grundzüge der Mengenlehre" ("Basics of Set Theory"), p. 32, in 1914: 〈𝐴, 𝐵〉5 = {{𝐴, 𝑂}, {𝐵, 𝑇}}. Hausdorff used 1 and 2 instead of 𝑂 and 𝑇, but actually any two different fixed sets will do (e.g., 𝑂 = ∅ and 𝑇 = {∅}, see 0nep0 5281). Furthermore, Hausdorff demanded that 𝑂 and 𝑇 are both different from 𝐴 as well as 𝐵, which is actually not necessary (at least not in full extent), see opthhausdorff0 5433 and opthhausdorff 5432. If we restrict our sets to nonnegative integers, an ordered pair definition that involves only elementary arithmetic is provided by nn0opthi 13993. An ordered pair of real numbers can also be represented by a complex number as shown by cru 11974. Kuratowski's ordered pair definition is standard for ZFC set theory, but it is very inconvenient to use in New Foundations theory because it is not type-level; a common alternate definition in New Foundations is the definition from [Rosser] p. 281. Since there are other ways to define ordered pairs, we discourage direct use of this definition so that most theorems won't depend on this particular construction; theorems will instead rely on dfopif 4801. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.) |
⊢ 〈𝐴, 𝐵〉 = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})} | ||
Syntax | cotp 4570 | Extend class notation to include ordered triple. |
class 〈𝐴, 𝐵, 𝐶〉 | ||
Definition | df-ot 4571 | Define ordered triple of classes. Definition of ordered triple in [Stoll] p. 25. (Contributed by NM, 3-Apr-2015.) |
⊢ 〈𝐴, 𝐵, 𝐶〉 = 〈〈𝐴, 𝐵〉, 𝐶〉 | ||
Theorem | sneq 4572 | Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | ||
Theorem | sneqi 4573 | Equality inference for singletons. (Contributed by NM, 22-Jan-2004.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ {𝐴} = {𝐵} | ||
Theorem | sneqd 4574 | Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐴} = {𝐵}) | ||
Theorem | dfsn2 4575 | Alternate definition of singleton. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.) |
⊢ {𝐴} = {𝐴, 𝐴} | ||
Theorem | elsng 4576 | There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15 (generalized). (Contributed by NM, 13-Sep-1995.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | ||
Theorem | elsn 4577 | There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵) | ||
Theorem | velsn 4578 | There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | ||
Theorem | elsni 4579 | There is at most one element in a singleton. (Contributed by NM, 5-Jun-1994.) |
⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵) | ||
Theorem | absn 4580* | Condition for a class abstraction to be a singleton. Formerly part of proof of dfiota2 6396. (Contributed by Andrew Salmon, 30-Jun-2011.) (Revised by AV, 24-Aug-2022.) |
⊢ ({𝑥 ∣ 𝜑} = {𝑌} ↔ ∀𝑥(𝜑 ↔ 𝑥 = 𝑌)) | ||
Theorem | dfpr2 4581* | Alternate definition of a pair. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.) |
⊢ {𝐴, 𝐵} = {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵)} | ||
Theorem | dfsn2ALT 4582 | Alternate definition of singleton, based on the (alternate) definition of pair. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by AV, 12-Jun-2022.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ {𝐴} = {𝐴, 𝐴} | ||
Theorem | elprg 4583 | A member of a pair of classes is one or the other of them, and conversely as soon as it is a set. Exercise 1 of [TakeutiZaring] p. 15, generalized. (Contributed by NM, 13-Sep-1995.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | ||
Theorem | elpri 4584 | If a class is an element of a pair, then it is one of the two paired elements. (Contributed by Scott Fenton, 1-Apr-2011.) |
⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) | ||
Theorem | elpr 4585 | A member of a pair of classes is one or the other of them, and conversely as soon as it is a set. Exercise 1 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) | ||
Theorem | elpr2g 4586 | A member of a pair of sets is one or the other of them, and conversely. Exercise 1 of [TakeutiZaring] p. 15. (Contributed by NM, 14-Oct-2005.) Generalize from sethood hypothesis to sethood antecedent. (Revised by BJ, 25-May-2024.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | ||
Theorem | elpr2 4587 | A member of a pair of sets is one or the other of them, and conversely. Exercise 1 of [TakeutiZaring] p. 15. (Contributed by NM, 14-Oct-2005.) (Proof shortened by JJ, 23-Jul-2021.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) | ||
Theorem | elpr2OLD 4588 | Obsolete version of elpr2 4587 as of 25-May-2024. (Contributed by NM, 14-Oct-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) | ||
Theorem | nelpr2 4589 | If a class is not an element of an unordered pair, it is not the second listed element. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶}) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) | ||
Theorem | nelpr1 4590 | If a class is not an element of an unordered pair, it is not the first listed element. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶}) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) | ||
Theorem | nelpri 4591 | If an element doesn't match the items in an unordered pair, it is not in the unordered pair. (Contributed by David A. Wheeler, 10-May-2015.) |
⊢ 𝐴 ≠ 𝐵 & ⊢ 𝐴 ≠ 𝐶 ⇒ ⊢ ¬ 𝐴 ∈ {𝐵, 𝐶} | ||
Theorem | prneli 4592 | If an element doesn't match the items in an unordered pair, it is not in the unordered pair, using ∉. (Contributed by David A. Wheeler, 10-May-2015.) |
⊢ 𝐴 ≠ 𝐵 & ⊢ 𝐴 ≠ 𝐶 ⇒ ⊢ 𝐴 ∉ {𝐵, 𝐶} | ||
Theorem | nelprd 4593 | If an element doesn't match the items in an unordered pair, it is not in the unordered pair, deduction version. (Contributed by Alexander van der Vekens, 25-Jan-2018.) |
⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶}) | ||
Theorem | eldifpr 4594 | Membership in a set with two elements removed. Similar to eldifsn 4721 and eldiftp 4623. (Contributed by Mario Carneiro, 18-Jul-2017.) |
⊢ (𝐴 ∈ (𝐵 ∖ {𝐶, 𝐷}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷)) | ||
Theorem | rexdifpr 4595 | Restricted existential quantification over a set with two elements removed. (Contributed by Alexander van der Vekens, 7-Feb-2018.) |
⊢ (∃𝑥 ∈ (𝐴 ∖ {𝐵, 𝐶})𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ∧ 𝜑)) | ||
Theorem | snidg 4596 | A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 28-Oct-2003.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) | ||
Theorem | snidb 4597 | A class is a set iff it is a member of its singleton. (Contributed by NM, 5-Apr-2004.) |
⊢ (𝐴 ∈ V ↔ 𝐴 ∈ {𝐴}) | ||
Theorem | snid 4598 | A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 31-Dec-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ 𝐴 ∈ {𝐴} | ||
Theorem | vsnid 4599 | A setvar variable is a member of its singleton. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 𝑥 ∈ {𝑥} | ||
Theorem | elsn2g 4600 | There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. This variation requires only that 𝐵, rather than 𝐴, be a set. (Contributed by NM, 28-Oct-2003.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |