mmtheorems24 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10658

Statement List for Metamath Proof Explorer - 2301-2400 - Page 24 of 107

Type	Label	Description
Statement
Theorem	ssne0 2301	A class with a nonempty subclass is nonempty.
⊢ ((A ⊆ B ⋀ A ≠ ∅) → B ≠ ∅)
Theorem	un00 2302	Two classes are empty iff their union is empty.
⊢ ((A = ∅ ⋀ B = ∅) ↔ (A ∪ B) = ∅)
Theorem	vss 2303	Only the universal class has the universal class as a subclass.
⊢ (V ⊆ A ↔ A = V)
Theorem	0pss 2304	The null set is a proper subset of any non-empty set.
⊢ (∅ ⊂ A ↔ A ≠ ∅)
Theorem	npss0 2305	No set is a proper subset of the empty set.
⊢ ¬ A ⊂ ∅
Theorem	pssv 2306	Any non-universal class is a proper subclass of the universal class.
⊢ (A ⊂ V ↔ ¬ A = V)
Theorem	disj 2307	Two ways of saying that two classes are disjoint (have no members in common).
⊢ ((A ∩ B) = ∅ ↔ ∀x ∈ A ¬ x ∈ B)
Theorem	disj1 2308	Two ways of saying that two classes are disjoint (have no members in common).
⊢ ((A ∩ B) = ∅ ↔ ∀x(x ∈ A → ¬ x ∈ B))
Theorem	reldisj 2309	Two ways of saying that two classes are disjoint, using the complement of B relative to a universe C.
⊢ (A ⊆ C → ((A ∩ B) = ∅ ↔ A ⊆ (C ∖ B)))
Theorem	disj3 2310	Two ways of saying that two classes are disjoint.
⊢ ((A ∩ B) = ∅ ↔ A = (A ∖ B))
Theorem	disjne 2311	Members of disjoint sets are not equal.
⊢ (((A ∩ B) = ∅ ⋀ C ∈ A ⋀ D ∈ B) → C ≠ D)
Theorem	disj2 2312	Two ways of saying that two classes are disjoint.
⊢ ((A ∩ B) = ∅ ↔ A ⊆ (V ∖ B))
Theorem	disj4 2313	Two ways of saying that two classes are disjoint.
⊢ ((A ∩ B) = ∅ ↔ ¬ (A ∖ B) ⊂ A)
Theorem	ssdisj 2314	Intersection with a subclass of a disjoint class. (Contributed by FL, 24-Jan-2007.)
⊢ ((A ⊆ B ⋀ (B ∩ C) = ∅) → (A ∩ C) = ∅)
Theorem	disjpss 2315	A class is a proper subset of its union with a disjoint nonempty class.
⊢ (((A ∩ B) = ∅ ⋀ B ≠ ∅) → A ⊂ (A ∪ B))
Theorem	undisj1 2316	The union of disjoint classes is disjoint.
⊢ (((A ∩ C) = ∅ ⋀ (B ∩ C) = ∅) ↔ ((A ∪ B) ∩ C) = ∅)
Theorem	undisj2 2317	The union of disjoint classes is disjoint.
⊢ (((A ∩ B) = ∅ ⋀ (A ∩ C) = ∅) ↔ (A ∩ (B ∪ C)) = ∅)
Theorem	ssindif0 2318	Subclass expressed in terms of intersection with difference from the universal class.
⊢ (A ⊆ B ↔ (A ∩ (V ∖ B)) = ∅)
Theorem	inelcm 2319	The intersection of classes with a common member is nonempty.
⊢ ((A ∈ B ⋀ A ∈ C) → (B ∩ C) ≠ ∅)
Theorem	minel 2320	A minimum element of a class has no elements in common with the class.
⊢ ((A ∈ B ⋀ (C ∩ B) = ∅) → ¬ A ∈ C)
Theorem	undif4 2321	Distribute union over difference.
⊢ ((A ∩ C) = ∅ → (A ∪ (B ∖ C)) = ((A ∪ B) ∖ C))
Theorem	disjssun 2322	Subset relation for disjoint classes.
⊢ ((A ∩ B) = ∅ → (A ⊆ (B ∪ C) ↔ A ⊆ C))
Theorem	ssdif0 2323	Subclass expressed in terms of difference. Exercise 7 of [TakeutiZaring] p. 22.
⊢ (A ⊆ B ↔ (A ∖ B) = ∅)
Theorem	vdif0 2324	Universal class equality in terms of empty difference.
⊢ (A = V ↔ (V ∖ A) = ∅)
Theorem	pssdifn0 2325	A proper subclass has a nonempty difference.
⊢ ((A ⊆ B ⋀ A ≠ B) → (B ∖ A) ≠ ∅)
Theorem	ssnelpss 2326	A subclass missing a member is a proper subclass.
⊢ (A ⊆ B → ((C ∈ B ⋀ ¬ C ∈ A) → A ⊂ B))
Theorem	pssnel 2327	A proper subclass has a member in one argument that's not in both.
⊢ (A ⊂ B → ∃x(x ∈ B ⋀ ¬ x ∈ A))
Theorem	difin0ss 2328	Difference, intersection, and subclass relationship.
⊢ (((A ∖ B) ∩ C) = ∅ → (C ⊆ A → C ⊆ B))
Theorem	inssdif0 2329	Intersection, subclass, and difference relationship.
⊢ ((A ∩ B) ⊆ C ↔ (A ∩ (B ∖ C)) = ∅)
Theorem	difid 2330	The difference between a class and itself is the empty set. Proposition 5.15 of [TakeutiZaring] p. 20. Also Theorem 32 of [Suppes] p. 28.
⊢ (A ∖ A) = ∅
Theorem	dif0 2331	The difference between a class and the empty set. Part of Exercise 4.4 of [Stoll] p. 16.
⊢ (A ∖ ∅) = A
Theorem	0dif 2332	The difference between the empty set and a class. Part of Exercise 4.4 of [Stoll] p. 16.
⊢ (∅ ∖ A) = ∅
Theorem	difdisj 2333	A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29.
⊢ (A ∩ (B ∖ A)) = ∅
Theorem	difin0 2334	The difference of a class from its intersection is empty. Theorem 37 of [Suppes] p. 29.
⊢ ((A ∩ B) ∖ B) = ∅
Theorem	undifv 2335	The union of a class and its complement is the universe. Theorem 5.1(5) of [Stoll] p. 17.
⊢ (A ∪ (V ∖ A)) = V
Theorem	undif1 2336	Absorption of difference by union. This decomposes a union into two disjoint classes (see difdisj 2333). Theorem 35 of [Suppes] p. 29.
⊢ ((A ∖ B) ∪ B) = (A ∪ B)
Theorem	undif2 2337	Absorption of difference by union. This decomposes a union into two disjoint classes (see difdisj 2333). Part of proof of Corollary 6K of [Enderton] p. 144.
⊢ (A ∪ (B ∖ A)) = (A ∪ B)
Theorem	difun2 2338	Absorption of union by difference. Theorem 36 of [Suppes] p. 29.
⊢ ((A ∪ B) ∖ B) = (A ∖ B)
Theorem	undif 2339	Union of complementary parts into whole.
⊢ (A ⊆ B ↔ (A ∪ (B ∖ A)) = B)
Theorem	ssundif 2340	A condition equivalent to inclusion in the union of two classes.
⊢ (A ⊆ (B ∪ C) ↔ (A ∖ B) ⊆ C)
Theorem	difcom 2341	Swap the arguments of a class difference.
⊢ ((A ∖ B) ⊆ C ↔ (A ∖ C) ⊆ B)
Theorem	difdifdir 2342	Distributive law for class difference. Exercise 4.8 of [Stoll] p. 16.
⊢ ((A ∖ B) ∖ C) = ((A ∖ C) ∖ (B ∖ C))
Theorem	r19.2z 2343	Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1028). The restricted version is valid only when the domain of quantification is not empty.
⊢ ((A ≠ ∅ ⋀ ∀x ∈ A φ) → ∃x ∈ A φ)
Theorem	r19.3rzv 2344	Restricted quantification of wff not containing quantified variable.
⊢ (A ≠ ∅ → (φ ↔ ∀x ∈ A φ))
Theorem	r19.9rzv 2345	Restricted quantification of wff not containing quantified variable.
⊢ (A ≠ ∅ → (φ ↔ ∃x ∈ A φ))
Theorem	r19.28zv 2346	Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty.
⊢ (A ≠ ∅ → (∀x ∈ A (φ ⋀ ψ) ↔ (φ ⋀ ∀x ∈ A ψ)))
Theorem	r19.37zv 2347	Restricted quantifier version of Theorem 19.37 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty. (Contributed by Paul Chapman, 8-Oct-2007.)
⊢ (A ≠ ∅ → (∃x ∈ A (φ → ψ) ↔ (φ → ∃x ∈ A ψ)))
Theorem	r19.45zv 2348	Restricted version of Theorem 19.45 of [Margaris] p. 90.
⊢ (A ≠ ∅ → (∃x ∈ A (φ ⋁ ψ) ↔ (φ ⋁ ∃x ∈ A ψ)))
Theorem	r19.27zv 2349	Restricted quantifier version of Theorem 19.27 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty.
⊢ (A ≠ ∅ → (∀x ∈ A (φ ⋀ ψ) ↔ (∀x ∈ A φ ⋀ ψ)))
Theorem	r19.36zv 2350	Restricted quantifier version of Theorem 19.36 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty.
⊢ (A ≠ ∅ → (∃x ∈ A (φ → ψ) ↔ (∀x ∈ A φ → ψ)))
Theorem	rzal 2351	Vacuous quantification is always true.
⊢ (A = ∅ → ∀x ∈ A φ)
Theorem	rexn0 2352	Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
⊢ (∃x ∈ A φ → A ≠ ∅)
Theorem	ralidm 2353	Idempotent law for restricted quantifier.
⊢ (∀x ∈ A ∀x ∈ A φ ↔ ∀x ∈ A φ)
Theorem	ral0 2354	Vacuous universal quantification is always true.
⊢ ∀x ∈ ∅ φ
Theorem	ralf0 2355	The quantification of a falsehood is vacuous when true.
⊢ ¬ φ    ⇒   ⊢ (∀x ∈ A φ ↔ A = ∅)
Theorem	raaan 2356	Rearrange restricted quantifiers.
⊢ (∀x ∈ A ∀y ∈ A (φ ⋀ ψ) ↔ (∀x ∈ A φ ⋀ ∀y ∈ A ψ))
"Weak deduction theorem" for set theory
Syntax	cif 2357	Extend class notation to include the conditional operator. See df-if 2358 for a description. (In older databases this was denoted "ded".)
class if(φ, A, B)
Definition	df-if 2358	Define the conditional operator. Read if(φ, A, B) as "if φ then A else B." See iftrue 2362 and iffalse 2363 for its values. In mathematical literature, this operator is rarely defined formally but is implicit in informal definitions such as "let f(x)=0 if x=0 and 1/x otherwise." (In older versions of this database, this operator was denoted "ded" and called the "deduction class.") An important use for us is in conjunction with the weak deduction theorem, which converts a hypothesis into an antecedent. In that role, A is a class variable in the hypothesis and B is a class (usually a constant) that makes the hypothesis true when it is substituted for A. See dedth 2379 for the main part of the weak deduction theorem, elimhyp 2386 to eliminate a hypothesis, and keephyp 2392 to keep a hypothesis. See the Deduction Theorem link on the Metamath Proof Explorer Home Page for a description of the weak deduction theorem.
⊢ if(φ, A, B) = {x∣((x ∈ A ⋀ φ) ⋁ (x ∈ B ⋀ ¬ φ))}
Theorem	dfif2 2359	An alternate definition of the conditional operator df-if 2358 with one fewer connectives (but probably less intuitive to understand).
⊢ if(φ, A, B) = {x∣((x ∈ B → φ) → (x ∈ A ⋀ φ))}
Theorem	ifeq1 2360	Equality theorem for conditional operator.
⊢ (A = B → if(φ, A, C) = if(φ, B, C))
Theorem	ifeq2 2361	Equality theorem for conditional operator.
⊢ (A = B → if(φ, C, A) = if(φ, C, B))
Theorem	iftrue 2362	Value of the conditional operator when its first argument is true.
⊢ (φ → if(φ, A, B) = A)
Theorem	iffalse 2363	Value of the conditional operator when its first argument is false.
⊢ (¬ φ → if(φ, A, B) = B)
Theorem	ifeq12 2364	Equality theorem for conditional operators.
⊢ ((A = B ⋀ C = D) → if(φ, A, C) = if(φ, B, D))
Theorem	ifeq1d 2365	Equality deduction for conditional operator.
⊢ (φ → A = B)    ⇒   ⊢ (φ → if(ψ, A, C) = if(ψ, B, C))
Theorem	ifeq2d 2366	Equality deduction for conditional operator.
⊢ (φ → A = B)    ⇒   ⊢ (φ → if(ψ, C, A) = if(ψ, C, B))
Theorem	ifbi 2367	Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004.)
⊢ ((φ ↔ ψ) → if(φ, A, B) = if(ψ, A, B))
Theorem	ifbid 2368	Equivalence deduction for conditional operators.
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → if(ψ, A, B) = if(χ, A, B))
Theorem	hbif 2369	Bound-variable hypothesis builder for a conditional operator.
⊢ (φ → ∀xφ)    &   ⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (y ∈ B → ∀x y ∈ B)    ⇒   ⊢ (y ∈ if(φ, A, B) → ∀x y ∈ if(φ, A, B))
Theorem	elimif 2370	Elimination of a conditional operator contained in a wff ψ.
⊢ ( if(φ, A, B) = A → (ψ ↔ χ))    &   ⊢ ( if(φ, A, B) = B → (ψ ↔ θ))    ⇒   ⊢ (ψ ↔ ((φ ⋀ χ) ⋁ (¬ φ ⋀ θ)))
Theorem	ifboth 2371	A wff θ containing a conditional operator is true when both of its cases are true.
⊢ (A = if(φ, A, B) → (ψ ↔ θ))    &   ⊢ (B = if(φ, A, B) → (χ ↔ θ))    ⇒   ⊢ ((ψ ⋀ χ) → θ)
Theorem	ifid 2372	Identical true and false arguments in the conditional operator.
⊢ if(φ, A, A) = A
Theorem	eqif 2373	Expansion of an equality with a conditional operator.
⊢ (A = if(φ, B, C) ↔ ((φ ⋀ A = B) ⋁ (¬ φ ⋀ A = C)))
Theorem	elif 2374	Membership in a conditional operator.
⊢ (A ∈ if(φ, B, C) ↔ ((φ ⋀ A ∈ B) ⋁ (¬ φ ⋀ A ∈ C)))
Theorem	ifel 2375	Membership of a conditional operator.
⊢ ( if(φ, A, B) ∈ C ↔ ((φ ⋀ A ∈ C) ⋁ (¬ φ ⋀ B ∈ C)))
Theorem	ifcl 2376	Membership (closure) of a conditional operator.
⊢ ((A ∈ C ⋀ B ∈ C) → if(φ, A, B) ∈ C)
Theorem	ifor 2377	The possible values of a conditional operator.
⊢ ( if(φ, A, B) = A ⋁ if(φ, A, B) = B)
Theorem	ifswap 2378	Negating the first argument swaps the last two arguments of a conditional operator.
⊢ if(¬ φ, A, B) = if(φ, B, A)
Theorem	dedth 2379	Weak deduction theorem that eliminates a hypothesis φ, making it become an antecedent. We assume that a proof exists for φ when the class variable A is replaced with a specific class B. The hypothesis χ should be assigned to the inference, and the inference's hypothesis eliminated with elimhyp 2386. If the inference has other hypotheses with class variable A, these can be kept by assigning keephyp 2392 to them. For more information, see the Deduction Theorem http://us.metamath.org/mpegif/mmdeduction.html.
⊢ (A = if(φ, A, B) → (ψ ↔ χ))    &   ⊢ χ    ⇒   ⊢ (φ → ψ)
Theorem	dedth2v 2380	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 2383 is simpler to use. See also comments in dedth 2379.
⊢ (A = if(φ, A, C) → (ψ ↔ χ))    &   ⊢ (B = if(φ, B, D) → (χ ↔ θ))    &   ⊢ θ    ⇒   ⊢ (φ → ψ)
Theorem	dedth3v 2381	Weak deduction theorem for eliminating a hypothesis with 3 class variables. See comments in dedth2v 2380.
⊢ (A = if(φ, A, D) → (ψ ↔ χ))    &   ⊢ (B = if(φ, B, R) → (χ ↔ θ))    &   ⊢ (C = if(φ, C, S) → (θ ↔ τ))    &   ⊢ τ    ⇒   ⊢ (φ → ψ)
Theorem	dedth4v 2382	Weak deduction theorem for eliminating a hypothesis with 4 class variables. See comments in dedth2v 2380.
⊢ (A = if(φ, A, R) → (ψ ↔ χ))    &   ⊢ (B = if(φ, B, S) → (χ ↔ θ))    &   ⊢ (C = if(φ, C, T) → (θ ↔ τ))    &   ⊢ (D = if(φ, D, U) → (τ ↔ η))    &   ⊢ η    ⇒   ⊢ (φ → ψ)
Theorem	dedth2h 2383	Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v 2380 but requires that each hypothesis has exactly one class variable. See also comments in dedth 2379.
⊢ (A = if(φ, A, C) → (χ ↔ θ))    &   ⊢ (B = if(ψ, B, D) → (θ ↔ τ))    &   ⊢ τ    ⇒   ⊢ ((φ ⋀ ψ) → χ)
Theorem	dedth3h 2384	Weak deduction theorem eliminating three hypotheses. See comments in dedth2h 2383.
⊢ (A = if(φ, A, D) → (θ ↔ τ))    &   ⊢ (B = if(ψ, B, R) → (τ ↔ η))    &   ⊢ (C = if(χ, C, S) → (η ↔ ζ))    &   ⊢ ζ    ⇒   ⊢ ((φ ⋀ ψ ⋀ χ) → θ)
Theorem	dedth4h 2385	Weak deduction theorem eliminating four hypotheses. See comments in dedth2h 2383.
⊢ (A = if(φ, A, R) → (τ ↔ η))    &   ⊢ (B = if(ψ, B, S) → (η ↔ ζ))    &   ⊢ (C = if(χ, C, F) → (ζ ↔ σ))    &   ⊢ (D = if(θ, D, G) → (σ ↔ ρ))    &   ⊢ ρ    ⇒   ⊢ (((φ ⋀ ψ) ⋀ (χ ⋀ θ)) → τ)
Theorem	elimhyp 2386	Eliminate a hypothesis containing class variable A when it is known for a specific class B. For more information, see comments in dedth 2379.
⊢ (A = if(φ, A, B) → (φ ↔ ψ))    &   ⊢ (B = if(φ, A, B) → (χ ↔ ψ))    &   ⊢ χ    ⇒   ⊢ ψ
Theorem	elimhyp2v 2387	Eliminate a hypothesis containing 2 class variables.
⊢ (A = if(φ, A, C) → (φ ↔ χ))    &   ⊢ (B = if(φ, B, D) → (χ ↔ θ))    &   ⊢ (C = if(φ, A, C) → (τ ↔ η))    &   ⊢ (D = if(φ, B, D) → (η ↔ θ))    &   ⊢ τ    ⇒   ⊢ θ
Theorem	elimhyp3v 2388	Eliminate a hypothesis containing 3 class variables.
⊢ (A = if(φ, A, D) → (φ ↔ χ))    &   ⊢ (B = if(φ, B, R) → (χ ↔ θ))    &   ⊢ (C = if(φ, C, S) → (θ ↔ τ))    &   ⊢ (D = if(φ, A, D) → (η ↔ ζ))    &   ⊢ (R = if(φ, B, R) → (ζ ↔ σ))    &   ⊢ (S = if(φ, C, S) → (σ ↔ τ))    &   ⊢ η    ⇒   ⊢ τ
Theorem	elimhyp4v 2389	Eliminate a hypothesis containing 4 class variables (for use with the weak deduction theorem dedth 2379).
⊢ (A = if(φ, A, D) → (φ ↔ χ))    &   ⊢ (B = if(φ, B, R) → (χ ↔ θ))    &   ⊢ (C = if(φ, C, S) → (θ ↔ τ))    &   ⊢ (F = if(φ, F, G) → (τ ↔ ψ))    &   ⊢ (D = if(φ, A, D) → (η ↔ ζ))    &   ⊢ (R = if(φ, B, R) → (ζ ↔ σ))    &   ⊢ (S = if(φ, C, S) → (σ ↔ ρ))    &   ⊢ (G = if(φ, F, G) → (ρ ↔ ψ))    &   ⊢ η    ⇒   ⊢ ψ
Theorem	elimel 2390	Eliminate a membership hypothesis for weak deduction theorem, when special case B ∈ C is provable.
⊢ B ∈ C    ⇒   ⊢ if(A ∈ C, A, B) ∈ C
Theorem	elimdhyp 2391	Version of elimhyp 2386 where the hypothesis is deduced from the final antecedent. See ghomgrplem 10328 for an example of its use. (Contributed by Paul Chapman, 25-Mar-2008.)
⊢ (φ → ψ)    &   ⊢ (A = if(φ, A, B) → (ψ ↔ χ))    &   ⊢ (B = if(φ, A, B) → (θ ↔ χ))    &   ⊢ θ    ⇒   ⊢ χ
Theorem	keephyp 2392	Transform a hypothesis ψ that we want to keep (but contains the same class variable A used in the eliminated hypothesis) for use with the weak deduction theorem.
⊢ (A = if(φ, A, B) → (ψ ↔ θ))    &   ⊢ (B = if(φ, A, B) → (χ ↔ θ))    &   ⊢ ψ    &   ⊢ χ    ⇒   ⊢ θ
Theorem	keephyp2v 2393	Keep a hypothesis containing 2 class variables (for use with the weak deduction theorem dedth 2379).
⊢ (A = if(φ, A, C) → (ψ ↔ χ))    &   ⊢ (B = if(φ, B, D) → (χ ↔ θ))    &   ⊢ (C = if(φ, A, C) → (τ ↔ η))    &   ⊢ (D = if(φ, B, D) → (η ↔ θ))    &   ⊢ ψ    &   ⊢ τ    ⇒   ⊢ θ
Theorem	keephyp3v 2394	Keep a hypothesis containing 3 class variables.
⊢ (A = if(φ, A, D) → (ρ ↔ χ))    &   ⊢ (B = if(φ, B, R) → (χ ↔ θ))    &   ⊢ (C = if(φ, C, S) → (θ ↔ τ))    &   ⊢ (D = if(φ, A, D) → (η ↔ ζ))    &   ⊢ (R = if(φ, B, R) → (ζ ↔ σ))    &   ⊢ (S = if(φ, C, S) → (σ ↔ τ))    &   ⊢ ρ    &   ⊢ η    ⇒   ⊢ τ
Theorem	keepel 2395	Keep a membership hypothesis for weak deduction theorem, when special case B ∈ C is provable.
⊢ A ∈ C    &   ⊢ B ∈ C    ⇒   ⊢ if(φ, A, B) ∈ C
Theorem	ifex 2396	Conditional operator existence.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ if(φ, A, B) ∈ V
Power classes
Syntax	cpw 2397	Extend class notation to include power class. (The tilde in the Metamath token is meant to suggest the calligraphic font of the P.)
class ℘A
Definition	df-pw 2398	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.
⊢ ℘A = {x∣x ⊆ A}
Theorem	pweq 2399	Equality theorem for the power class.
⊢ (A = B → ℘A = ℘B)
Theorem	elpw 2400	Membership in a power class. Theorem 86 of [Suppes] p. 47.
⊢ A ∈ V    ⇒   ⊢ (A ∈ ℘B ↔ A ⊆ B)