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	ifeq12da 4501	Equivalence deduction for conditional operators. (Contributed by Wolf Lammen, 24-Jun-2021.)
⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)    &   ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜓, 𝐶, 𝐷))
Theorem	ifbieq12d2 4502	Equivalence deduction for conditional operators. (Contributed by Thierry Arnoux, 14-Feb-2017.) (Proof shortened by Wolf Lammen, 24-Jun-2021.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)    &   ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))
Theorem	ifclda 4503	Conditional closure. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
Theorem	ifeqda 4504	Separation of the values of the conditional operator. (Contributed by Alexander van der Vekens, 13-Apr-2018.)
⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)    &   ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶)
Theorem	elimif 4505	Elimination of a conditional operator contained in a wff 𝜓. (Contributed by NM, 15-Feb-2005.) (Proof shortened by NM, 25-Apr-2019.)
⊢ (if(𝜑, 𝐴, 𝐵) = 𝐴 → (𝜓 ↔ 𝜒))    &   ⊢ (if(𝜑, 𝐴, 𝐵) = 𝐵 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜓 ↔ ((𝜑 ∧ 𝜒) ∨ (¬ 𝜑 ∧ 𝜃)))
Theorem	ifbothda 4506	A wff 𝜃 containing a conditional operator is true when both of its cases are true. (Contributed by NM, 15-Feb-2015.)
⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃))    &   ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃))    &   ⊢ ((𝜂 ∧ 𝜑) → 𝜓)    &   ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜒)    ⇒   ⊢ (𝜂 → 𝜃)
Theorem	ifboth 4507	A wff 𝜃 containing a conditional operator is true when both of its cases are true. (Contributed by NM, 3-Sep-2006.) (Revised by Mario Carneiro, 15-Feb-2015.)
⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃))    &   ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃))    ⇒   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
Theorem	ifid 4508	Identical true and false arguments in the conditional operator. (Contributed by NM, 18-Apr-2005.)
⊢ if(𝜑, 𝐴, 𝐴) = 𝐴
Theorem	eqif 4509	Expansion of an equality with a conditional operator. (Contributed by NM, 14-Feb-2005.)
⊢ (𝐴 = if(𝜑, 𝐵, 𝐶) ↔ ((𝜑 ∧ 𝐴 = 𝐵) ∨ (¬ 𝜑 ∧ 𝐴 = 𝐶)))
Theorem	ifval 4510	Another expression of the value of the if predicate, analogous to eqif 4509. See also the more specialized iftrue 4473 and iffalse 4476. (Contributed by BJ, 6-Apr-2019.)
⊢ (𝐴 = if(𝜑, 𝐵, 𝐶) ↔ ((𝜑 → 𝐴 = 𝐵) ∧ (¬ 𝜑 → 𝐴 = 𝐶)))
Theorem	elif 4511	Membership in a conditional operator. (Contributed by NM, 14-Feb-2005.)
⊢ (𝐴 ∈ if(𝜑, 𝐵, 𝐶) ↔ ((𝜑 ∧ 𝐴 ∈ 𝐵) ∨ (¬ 𝜑 ∧ 𝐴 ∈ 𝐶)))
Theorem	ifel 4512	Membership of a conditional operator. (Contributed by NM, 10-Sep-2005.)
⊢ (if(𝜑, 𝐴, 𝐵) ∈ 𝐶 ↔ ((𝜑 ∧ 𝐴 ∈ 𝐶) ∨ (¬ 𝜑 ∧ 𝐵 ∈ 𝐶)))
Theorem	ifcl 4513	Membership (closure) of a conditional operator. (Contributed by NM, 4-Apr-2005.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶)
Theorem	ifcld 4514	Membership (closure) of a conditional operator, deduction form. (Contributed by SO, 16-Jul-2018.)
⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
Theorem	ifcli 4515	Inference associated with ifcl 4513. Membership (closure) of a conditional operator. Also usable to keep a membership hypothesis for the weak deduction theorem dedth 4526 when the special case 𝐵 ∈ 𝐶 is provable. (Contributed by NM, 14-Aug-1999.) (Proof shortened by BJ, 1-Sep-2022.)
⊢ 𝐴 ∈ 𝐶    &   ⊢ 𝐵 ∈ 𝐶    ⇒   ⊢ if(𝜑, 𝐴, 𝐵) ∈ 𝐶
Theorem	ifexd 4516	Existence of the conditional operator (deduction form). (Contributed by SN, 26-Jul-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ V)
Theorem	ifexg 4517	Existence of the conditional operator (closed form). (Contributed by NM, 21-Mar-2011.) (Proof shortened by BJ, 1-Sep-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → if(𝜑, 𝐴, 𝐵) ∈ V)
Theorem	ifex 4518	Existence of the conditional operator (inference form). (Contributed by NM, 2-Sep-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ if(𝜑, 𝐴, 𝐵) ∈ V
Theorem	ifeqor 4519	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 4520	Negating the first argument swaps the last two arguments of a conditional operator. (Contributed by NM, 21-Jun-2007.)
⊢ if(¬ 𝜑, 𝐴, 𝐵) = if(𝜑, 𝐵, 𝐴)
Theorem	ifan 4521	Rewrite a conjunction in a conditional as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014.)
⊢ if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵)
Theorem	ifor 4522	Rewrite a disjunction in a conditional as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014.)
⊢ if((𝜑 ∨ 𝜓), 𝐴, 𝐵) = if(𝜑, 𝐴, if(𝜓, 𝐴, 𝐵))
Theorem	2if2 4523	Resolve two nested conditionals. (Contributed by Alexander van der Vekens, 27-Mar-2018.)
⊢ ((𝜑 ∧ 𝜓) → 𝐷 = 𝐴)    &   ⊢ ((𝜑 ∧ ¬ 𝜓 ∧ 𝜃) → 𝐷 = 𝐵)    &   ⊢ ((𝜑 ∧ ¬ 𝜓 ∧ ¬ 𝜃) → 𝐷 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐷 = if(𝜓, 𝐴, if(𝜃, 𝐵, 𝐶)))
Theorem	ifcomnan 4524	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 4525	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 1083. For more information on the weak deduction theorem, see the Weak Deduction Theorem page mmdeduction.html 1083. 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 4526	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 4533. If the inference has other hypotheses with class variable 𝐴, these can be kept by assigning keephyp 4539 to them. For more information, see the Weak Deduction Theorem page mmdeduction.html 4539. (Contributed by NM, 15-May-1999.)
⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜒))    &   ⊢ 𝜒    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	dedth2h 4527	Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v 4530 but requires that each hypothesis have exactly one class variable. See also comments in dedth 4526. (Contributed by NM, 15-May-1999.)
⊢ (𝐴 = if(𝜑, 𝐴, 𝐶) → (𝜒 ↔ 𝜃))    &   ⊢ (𝐵 = if(𝜓, 𝐵, 𝐷) → (𝜃 ↔ 𝜏))    &   ⊢ 𝜏    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	dedth3h 4528	Weak deduction theorem eliminating three hypotheses. See comments in dedth2h 4527. (Contributed by NM, 15-May-1999.)
⊢ (𝐴 = if(𝜑, 𝐴, 𝐷) → (𝜃 ↔ 𝜏))    &   ⊢ (𝐵 = if(𝜓, 𝐵, 𝑅) → (𝜏 ↔ 𝜂))    &   ⊢ (𝐶 = if(𝜒, 𝐶, 𝑆) → (𝜂 ↔ 𝜁))    &   ⊢ 𝜁    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	dedth4h 4529	Weak deduction theorem eliminating four hypotheses. See comments in dedth2h 4527. (Contributed by NM, 16-May-1999.)
⊢ (𝐴 = if(𝜑, 𝐴, 𝑅) → (𝜏 ↔ 𝜂))    &   ⊢ (𝐵 = if(𝜓, 𝐵, 𝑆) → (𝜂 ↔ 𝜁))    &   ⊢ (𝐶 = if(𝜒, 𝐶, 𝐹) → (𝜁 ↔ 𝜎))    &   ⊢ (𝐷 = if(𝜃, 𝐷, 𝐺) → (𝜎 ↔ 𝜌))    &   ⊢ 𝜌    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
Theorem	dedth2v 4530	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 4527 is simpler to use. See also comments in dedth 4526. (Contributed by NM, 13-Aug-1999.) (Proof shortened by Eric Schmidt, 28-Jul-2009.)
⊢ (𝐴 = if(𝜑, 𝐴, 𝐶) → (𝜓 ↔ 𝜒))    &   ⊢ (𝐵 = if(𝜑, 𝐵, 𝐷) → (𝜒 ↔ 𝜃))    &   ⊢ 𝜃    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	dedth3v 4531	Weak deduction theorem for eliminating a hypothesis with 3 class variables. See comments in dedth2v 4530. (Contributed by NM, 13-Aug-1999.) (Proof shortened by Eric Schmidt, 28-Jul-2009.)
⊢ (𝐴 = if(𝜑, 𝐴, 𝐷) → (𝜓 ↔ 𝜒))    &   ⊢ (𝐵 = if(𝜑, 𝐵, 𝑅) → (𝜒 ↔ 𝜃))    &   ⊢ (𝐶 = if(𝜑, 𝐶, 𝑆) → (𝜃 ↔ 𝜏))    &   ⊢ 𝜏    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	dedth4v 4532	Weak deduction theorem for eliminating a hypothesis with 4 class variables. See comments in dedth2v 4530. (Contributed by NM, 21-Apr-2007.) (Proof shortened by Eric Schmidt, 28-Jul-2009.)
⊢ (𝐴 = if(𝜑, 𝐴, 𝑅) → (𝜓 ↔ 𝜒))    &   ⊢ (𝐵 = if(𝜑, 𝐵, 𝑆) → (𝜒 ↔ 𝜃))    &   ⊢ (𝐶 = if(𝜑, 𝐶, 𝑇) → (𝜃 ↔ 𝜏))    &   ⊢ (𝐷 = if(𝜑, 𝐷, 𝑈) → (𝜏 ↔ 𝜂))    &   ⊢ 𝜂    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	elimhyp 4533	Eliminate a hypothesis containing class variable 𝐴 when it is known for a specific class 𝐵. For more information, see comments in dedth 4526. (Contributed by NM, 15-May-1999.)
⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜑 ↔ 𝜓))    &   ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜓))    &   ⊢ 𝜒    ⇒   ⊢ 𝜓
Theorem	elimhyp2v 4534	Eliminate a hypothesis containing 2 class variables. (Contributed by NM, 14-Aug-1999.)
⊢ (𝐴 = if(𝜑, 𝐴, 𝐶) → (𝜑 ↔ 𝜒))    &   ⊢ (𝐵 = if(𝜑, 𝐵, 𝐷) → (𝜒 ↔ 𝜃))    &   ⊢ (𝐶 = if(𝜑, 𝐴, 𝐶) → (𝜏 ↔ 𝜂))    &   ⊢ (𝐷 = if(𝜑, 𝐵, 𝐷) → (𝜂 ↔ 𝜃))    &   ⊢ 𝜏    ⇒   ⊢ 𝜃
Theorem	elimhyp3v 4535	Eliminate a hypothesis containing 3 class variables. (Contributed by NM, 14-Aug-1999.)
⊢ (𝐴 = if(𝜑, 𝐴, 𝐷) → (𝜑 ↔ 𝜒))    &   ⊢ (𝐵 = if(𝜑, 𝐵, 𝑅) → (𝜒 ↔ 𝜃))    &   ⊢ (𝐶 = if(𝜑, 𝐶, 𝑆) → (𝜃 ↔ 𝜏))    &   ⊢ (𝐷 = if(𝜑, 𝐴, 𝐷) → (𝜂 ↔ 𝜁))    &   ⊢ (𝑅 = if(𝜑, 𝐵, 𝑅) → (𝜁 ↔ 𝜎))    &   ⊢ (𝑆 = if(𝜑, 𝐶, 𝑆) → (𝜎 ↔ 𝜏))    &   ⊢ 𝜂    ⇒   ⊢ 𝜏
Theorem	elimhyp4v 4536	Eliminate a hypothesis containing 4 class variables (for use with the weak deduction theorem dedth 4526). (Contributed by NM, 16-Apr-2005.)
⊢ (𝐴 = if(𝜑, 𝐴, 𝐷) → (𝜑 ↔ 𝜒))    &   ⊢ (𝐵 = if(𝜑, 𝐵, 𝑅) → (𝜒 ↔ 𝜃))    &   ⊢ (𝐶 = if(𝜑, 𝐶, 𝑆) → (𝜃 ↔ 𝜏))    &   ⊢ (𝐹 = if(𝜑, 𝐹, 𝐺) → (𝜏 ↔ 𝜓))    &   ⊢ (𝐷 = if(𝜑, 𝐴, 𝐷) → (𝜂 ↔ 𝜁))    &   ⊢ (𝑅 = if(𝜑, 𝐵, 𝑅) → (𝜁 ↔ 𝜎))    &   ⊢ (𝑆 = if(𝜑, 𝐶, 𝑆) → (𝜎 ↔ 𝜌))    &   ⊢ (𝐺 = if(𝜑, 𝐹, 𝐺) → (𝜌 ↔ 𝜓))    &   ⊢ 𝜂    ⇒   ⊢ 𝜓
Theorem	elimel 4537	Eliminate a membership hypothesis for weak deduction theorem, when special case 𝐵 ∈ 𝐶 is provable. (Contributed by NM, 15-May-1999.)
⊢ 𝐵 ∈ 𝐶    ⇒   ⊢ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶
Theorem	elimdhyp 4538	Version of elimhyp 4533 where the hypothesis is deduced from the final antecedent. See divalg 16361 for an example of its use. (Contributed by Paul Chapman, 25-Mar-2008.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜒))    &   ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜃 ↔ 𝜒))    &   ⊢ 𝜃    ⇒   ⊢ 𝜒
Theorem	keephyp 4539	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 4540	Keep a hypothesis containing 2 class variables (for use with the weak deduction theorem dedth 4526). (Contributed by NM, 16-Apr-2005.)
⊢ (𝐴 = if(𝜑, 𝐴, 𝐶) → (𝜓 ↔ 𝜒))    &   ⊢ (𝐵 = if(𝜑, 𝐵, 𝐷) → (𝜒 ↔ 𝜃))    &   ⊢ (𝐶 = if(𝜑, 𝐴, 𝐶) → (𝜏 ↔ 𝜂))    &   ⊢ (𝐷 = if(𝜑, 𝐵, 𝐷) → (𝜂 ↔ 𝜃))    &   ⊢ 𝜓    &   ⊢ 𝜏    ⇒   ⊢ 𝜃
Theorem	keephyp3v 4541	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 4542	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 4543*	Soundness justification theorem for df-pw 4544. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ {𝑥 ∣ 𝑥 ⊆ 𝐴} = {𝑦 ∣ 𝑦 ⊆ 𝐴}
Definition	df-pw 4544*	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 30519). We will later introduce the Axiom of Power Sets ax-pow 5300, which can be expressed in class notation per pwexg 5313. Still later we will prove, in hashpw 14387, 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 4545	Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 5268. (Contributed by NM, 6-Aug-2000.) (Proof shortened by BJ, 31-Dec-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	elpw 4546	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 4547	Setvar variable membership in a power class. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
Theorem	elpwd 4548	Membership in a power class. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵)
Theorem	elpwi 4549	Subset relation implied by membership in a power class. (Contributed by NM, 17-Feb-2007.)
⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
Theorem	elpwb 4550	Characterization of the elements of a power class. (Contributed by BJ, 29-Apr-2021.)
⊢ (𝐴 ∈ 𝒫 𝐵 ↔ (𝐴 ∈ V ∧ 𝐴 ⊆ 𝐵))
Theorem	elpwid 4551	An element of a power class is a subclass. Deduction form of elpwi 4549. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	elelpwi 4552	If 𝐴 belongs to a part of 𝐶, then 𝐴 belongs to 𝐶. (Contributed by FL, 3-Aug-2009.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝒫 𝐶) → 𝐴 ∈ 𝐶)
Theorem	sspw 4553	The powerclass preserves inclusion. See sspwb 5394 for the biconditional version. (Contributed by NM, 13-Oct-1996.) Extract forward implication of sspwb 5394 since it requires fewer axioms. (Revised by BJ, 13-Apr-2024.)
⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
Theorem	sspwi 4554	The powerclass preserves inclusion (inference form). (Contributed by BJ, 13-Apr-2024.)
⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ 𝒫 𝐴 ⊆ 𝒫 𝐵
Theorem	sspwd 4555	The powerclass preserves inclusion (deduction form). (Contributed by BJ, 13-Apr-2024.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
Theorem	pweq 4556	Equality theorem for power class. (Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ, 13-Apr-2024.)
⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
Theorem	pweqALT 4557	Alternate proof of pweq 4556 directly from the definition. (Contributed by NM, 21-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
Theorem	pweqi 4558	Equality inference for power class. (Contributed by NM, 27-Nov-2013.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ 𝒫 𝐴 = 𝒫 𝐵
Theorem	pweqd 4559	Equality deduction for power class. (Contributed by NM, 27-Nov-2013.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → 𝒫 𝐴 = 𝒫 𝐵)
Theorem	pwunss 4560	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 5231, ax-nul 5241, ax-pr 5368 and shorten proof. (Revised by BJ, 13-Apr-2024.)
⊢ (𝒫 𝐴 ∪ 𝒫 𝐵) ⊆ 𝒫 (𝐴 ∪ 𝐵)
Theorem	nfpw 4561	Bound-variable hypothesis builder for power class. (Contributed by NM, 28-Oct-2003.) (Revised by Mario Carneiro, 13-Oct-2016.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥𝒫 𝐴
Theorem	pwidg 4562	A set is an element of its power set. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴)
Theorem	pwidb 4563	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 4564	A set is a member of its power class. Theorem 87 of [Suppes] p. 47. (Contributed by NM, 5-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ 𝐴 ∈ 𝒫 𝐴
Theorem	pwss 4565*	Subclass relationship for power class. (Contributed by NM, 21-Jun-2009.)
⊢ (𝒫 𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐵))
Theorem	pwundif 4566	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 5231, ax-nul 5241, ax-pr 5368 and shorten proof. (Revised by BJ, 14-Apr-2024.)
⊢ 𝒫 (𝐴 ∪ 𝐵) = ((𝒫 (𝐴 ∪ 𝐵) ∖ 𝒫 𝐴) ∪ 𝒫 𝐴)
2.1.18  Unordered and ordered pairs
Theorem	snjust 4567*	Soundness justification theorem for df-sn 4569. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ {𝑥 ∣ 𝑥 = 𝐴} = {𝑦 ∣ 𝑦 = 𝐴}
Syntax	csn 4568	Extend class notation to include singleton.
class {𝐴}
Definition	df-sn 4569*	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 4662. For an alternate definition see dfsn2 4581. (Contributed by NM, 21-Jun-1993.)
⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}
Syntax	cpr 4570	Extend class notation to include unordered pair.
class {𝐴, 𝐵}
Definition	df-pr 4571	Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For example, 𝐴 ∈ {1, -1} → (𝐴↑2) = 1 (ex-pr 30520). They are unordered, so {𝐴, 𝐵} = {𝐵, 𝐴} as proven by prcom 4677. For a more traditional definition, but requiring a dummy variable, see dfpr2 4589. {𝐴, 𝐴} is also an unordered pair, but also a singleton because of {𝐴} = {𝐴, 𝐴} (see dfsn2 4581). 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 4575. 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 4572	Extend class notation to include unordered triple (sometimes called "unordered triplet").
class {𝐴, 𝐵, 𝐶}
Definition	df-tp 4573	Define unordered triple of classes. Definition of [Enderton] p. 19. Note: ordered triples are a completely different object defined below in df-ot 4577. As with all tuples, when the term "triple" is used without qualifier, it means "ordered triple". (Contributed by NM, 9-Apr-1994.)
⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
Syntax	cop 4574	Extend class notation to include ordered pair.
class ⟨𝐴, 𝐵⟩
Definition	df-op 4575*	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 4841, opprc2 4842, and 0nelop 5442). For Kuratowski's actual definition when the arguments are sets, see dfop 4816. For the justifying theorem (for sets) see opth 5422. See dfopif 4814 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 4575 when the arguments are proper classes. Ordinarily this difference is not important, since neither definition is meaningful in that case. Our df-op 4575 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 5460. This was simplified by Kazimierz Kuratowski in 1921 to our present definition. An even simpler definition ⟨𝐴, 𝐵⟩3 = {𝐴, {𝐴, 𝐵}} is justified by opthreg 9528, 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 5686. 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 5293). 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 5464 and opthhausdorff 5463. If we restrict our sets to nonnegative integers, an ordered pair definition that involves only elementary arithmetic is provided by nn0opthi 14221. An ordered pair of real numbers can also be represented by a complex number as shown by cru 12140. 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 4814. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.) (Avoid depending on this detail.)
⊢ ⟨𝐴, 𝐵⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})}
Syntax	cotp 4576	Extend class notation to include ordered triple.
class ⟨𝐴, 𝐵, 𝐶⟩
Definition	df-ot 4577	Define ordered triple of classes. Definition of ordered triple in [Stoll] p. 25. (Contributed by NM, 3-Apr-2015.)
⊢ ⟨𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩
Theorem	sneq 4578	Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.)
⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
Theorem	sneqi 4579	Equality inference for singletons. (Contributed by NM, 22-Jan-2004.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ {𝐴} = {𝐵}
Theorem	sneqd 4580	Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝐴} = {𝐵})
Theorem	dfsn2 4581	Alternate definition of singleton. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.)
⊢ {𝐴} = {𝐴, 𝐴}
Theorem	elsng 4582	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 4583	There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)
Theorem	velsn 4584	There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.)
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
Theorem	elsni 4585	There is at most one element in a singleton. (Contributed by NM, 5-Jun-1994.)
⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
Theorem	elsnd 4586	There is at most one element in a singleton. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ (𝜑 → 𝐴 ∈ {𝐵})    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	rabsneq 4587*	Equality of class abstractions restricted to a singleton. (Contributed by AV, 17-May-2025.)
⊢ (𝑁 ∈ 𝑉 → {𝑥 ∈ {𝑁} ∣ 𝜓} = {𝑥 ∈ 𝑉 ∣ (𝑥 = 𝑁 ∧ 𝜓)})
Theorem	absn 4588*	Condition for a class abstraction to be a singleton. Formerly part of proof of dfiota2 6447. (Contributed by Andrew Salmon, 30-Jun-2011.) (Revised by AV, 24-Aug-2022.)
⊢ ({𝑥 ∣ 𝜑} = {𝑌} ↔ ∀𝑥(𝜑 ↔ 𝑥 = 𝑌))
Theorem	dfpr2 4589*	Alternate definition of a pair. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.)
⊢ {𝐴, 𝐵} = {𝑥 ∣ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵)}
Theorem	dfsn2ALT 4590	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 4591	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 4592	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 4593	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 4594	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 4595	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	elprn1 4596	A member of an unordered pair that is not the "first", must be the "second". (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ {𝐵, 𝐶} ∧ 𝐴 ≠ 𝐵) → 𝐴 = 𝐶)
Theorem	elprn2 4597	A member of an unordered pair that is not the "second", must be the "first". (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ {𝐵, 𝐶} ∧ 𝐴 ≠ 𝐶) → 𝐴 = 𝐵)
Theorem	nelpr2 4598	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 4599	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 4600	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.)
⊢ 𝐴 ≠ 𝐵    &   ⊢ 𝐴 ≠ 𝐶    ⇒   ⊢ ¬ 𝐴 ∈ {𝐵, 𝐶}