P. 46 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 4501-4600   *Has distinct variable group(s)

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([𝐴 / 𝑥]𝜑, ⦋𝐴 / 𝑥⦌𝐵, ⦋𝐴 / 𝑥⦌𝐶)
2.1.16  The weak deduction theorem for set theory 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(𝜑, 𝐶, 𝑆) → (𝜎 ↔ 𝜏))    &   ⊢ 𝜌    &   ⊢ 𝜂    ⇒   ⊢ 𝜏
2.1.17  Power classes
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.)
⊢ 𝒫 (𝐴 ∪ 𝐵) = ((𝒫 (𝐴 ∪ 𝐵) ∖ 𝒫 𝐴) ∪ 𝒫 𝐴)
2.1.18  Unordered and ordered pairs
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.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))