mmtheorems25 - 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-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Statement List for Metamath Proof Explorer - 2401-2500 - Page 25 of 123

Type	Label	Description
Statement
Theorem	r19.2z 2401	Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1066). The restricted version is valid only when the domain of quantification is not empty.
|- ((A =/= (/) /\ A.x e. A ph) -> E.x e. A ph)
Theorem	r19.3rzv 2402	Restricted quantification of wff not containing quantified variable.
|- (A =/= (/) -> (ph <-> A.x e. A ph))
Theorem	r19.9rzv 2403	Restricted quantification of wff not containing quantified variable.
|- (A =/= (/) -> (ph <-> E.x e. A ph))
Theorem	r19.28zv 2404	Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty.
|- (A =/= (/) -> (A.x e. A (ph /\ ps) <-> (ph /\ A.x e. A ps)))
Theorem	r19.37zv 2405	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 =/= (/) -> (E.x e. A (ph -> ps) <-> (ph -> E.x e. A ps)))
Theorem	r19.45zv 2406	Restricted version of Theorem 19.45 of [Margaris] p. 90.
|- (A =/= (/) -> (E.x e. A (ph \/ ps) <-> (ph \/ E.x e. A ps)))
Theorem	r19.27zv 2407	Restricted quantifier version of Theorem 19.27 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty.
|- (A =/= (/) -> (A.x e. A (ph /\ ps) <-> (A.x e. A ph /\ ps)))
Theorem	r19.36zv 2408	Restricted quantifier version of Theorem 19.36 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty.
|- (A =/= (/) -> (E.x e. A (ph -> ps) <-> (A.x e. A ph -> ps)))
Theorem	rzal 2409	Vacuous quantification is always true.
|- (A = (/) -> A.x e. A ph)
Theorem	rexn0 2410	Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
|- (E.x e. A ph -> A =/= (/))
Theorem	ralidm 2411	Idempotent law for restricted quantifier.
|- (A.x e. A A.x e. A ph <-> A.x e. A ph)
Theorem	ral0 2412	Vacuous universal quantification is always true.
|- A.x e. (/) ph
Theorem	ralf0 2413	The quantification of a falsehood is vacuous when true.
|- -. ph   =>   |- (A.x e. A ph <-> A = (/))
Theorem	raaan 2414	Rearrange restricted quantifiers.
|- (A.x e. A A.y e. A (ph /\ ps) <-> (A.x e. A ph /\ A.y e. A ps))
"Weak deduction theorem" for set theory
Syntax	cif 2415	Extend class notation to include the conditional operator. See df-if 2416 for a description. (In older databases this was denoted "ded".)
class if(ph, A, B)
Definition	df-if 2416	Define the conditional operator. Read if(ph, A, B) as "if ph then A else B." See iftrue 2420 and iffalse 2421 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 2437 for the main part of the weak deduction theorem, elimhyp 2447 to eliminate a hypothesis, and keephyp 2453 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(ph, A, B) = {x | ((x e. A /\ ph) \/ (x e. B /\ -. ph))}
Theorem	dfif2 2417	An alternate definition of the conditional operator df-if 2416 with one fewer connectives (but probably less intuitive to understand).
|- if(ph, A, B) = {x | ((x e. B -> ph) -> (x e. A /\ ph))}
Theorem	ifeq1 2418	Equality theorem for conditional operator.
|- (A = B -> if(ph, A, C) = if(ph, B, C))
Theorem	ifeq2 2419	Equality theorem for conditional operator.
|- (A = B -> if(ph, C, A) = if(ph, C, B))
Theorem	iftrue 2420	Value of the conditional operator when its first argument is true.
|- (ph -> if(ph, A, B) = A)
Theorem	iffalse 2421	Value of the conditional operator when its first argument is false.
|- (-. ph -> if(ph, A, B) = B)
Theorem	ifeq12 2422	Equality theorem for conditional operators.
|- ((A = B /\ C = D) -> if(ph, A, C) = if(ph, B, D))
Theorem	ifeq1d 2423	Equality deduction for conditional operator.
|- (ph -> A = B)   =>   |- (ph -> if(ps, A, C) = if(ps, B, C))
Theorem	ifeq2d 2424	Equality deduction for conditional operator.
|- (ph -> A = B)   =>   |- (ph -> if(ps, C, A) = if(ps, C, B))
Theorem	ifbi 2425	Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004.)
|- ((ph <-> ps) -> if(ph, A, B) = if(ps, A, B))
Theorem	ifbid 2426	Equivalence deduction for conditional operators.
|- (ph -> (ps <-> ch))   =>   |- (ph -> if(ps, A, B) = if(ch, A, B))
Theorem	hbif 2427	Bound-variable hypothesis builder for a conditional operator.
|- (ph -> A.xph)   &   |- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   =>   |- (y e. if(ph, A, B) -> A.x y e. if(ph, A, B))
Theorem	elimif 2428	Elimination of a conditional operator contained in a wff ps.
|- (if(ph, A, B) = A -> (ps <-> ch))   &   |- (if(ph, A, B) = B -> (ps <-> th))   =>   |- (ps <-> ((ph /\ ch) \/ (-. ph /\ th)))
Theorem	ifboth 2429	A wff th containing a conditional operator is true when both of its cases are true.
|- (A = if(ph, A, B) -> (ps <-> th))   &   |- (B = if(ph, A, B) -> (ch <-> th))   =>   |- ((ps /\ ch) -> th)
Theorem	ifid 2430	Identical true and false arguments in the conditional operator.
|- if(ph, A, A) = A
Theorem	eqif 2431	Expansion of an equality with a conditional operator.
|- (A = if(ph, B, C) <-> ((ph /\ A = B) \/ (-. ph /\ A = C)))
Theorem	elif 2432	Membership in a conditional operator.
|- (A e. if(ph, B, C) <-> ((ph /\ A e. B) \/ (-. ph /\ A e. C)))
Theorem	ifel 2433	Membership of a conditional operator.
|- (if(ph, A, B) e. C <-> ((ph /\ A e. C) \/ (-. ph /\ B e. C)))
Theorem	ifcl 2434	Membership (closure) of a conditional operator.
|- ((A e. C /\ B e. C) -> if(ph, A, B) e. C)
Theorem	ifor 2435	The possible values of a conditional operator.
|- (if(ph, A, B) = A \/ if(ph, A, B) = B)
Theorem	ifswap 2436	Negating the first argument swaps the last two arguments of a conditional operator.
|- if(-. ph, A, B) = if(ph, B, A)
Theorem	dedth 2437	Weak deduction theorem that eliminates a hypothesis ph, making it become an antecedent. We assume that a proof exists for ph when the class variable A is replaced with a specific class B. The hypothesis ch should be assigned to the inference, and the inference's hypothesis eliminated with elimhyp 2447. If the inference has other hypotheses with class variable A, these can be kept by assigning keephyp 2453 to them. For more information, see the Deduction Theorem http://us.metamath.org/mpegif/mmdeduction.html.
|- (A = if(ph, A, B) -> (ps <-> ch))   &   |- ch   =>   |- (ph -> ps)
Theorem	dedth2vOLD 2438	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 2441 is simpler to use. See also comments in dedth 2437.
|- (A = if(ph, A, C) -> (ps <-> ch))   &   |- (B = if(ph, B, D) -> (ch <-> th))   &   |- th   =>   |- (ph -> ps)
Theorem	dedth3vOLD 2439	Weak deduction theorem for eliminating a hypothesis with 3 class variables. See comments in dedth2v 2444.
|- (A = if(ph, A, D) -> (ps <-> ch))   &   |- (B = if(ph, B, R) -> (ch <-> th))   &   |- (C = if(ph, C, S) -> (th <-> ta))   &   |- ta   =>   |- (ph -> ps)
Theorem	dedth4vOLD 2440	Weak deduction theorem for eliminating a hypothesis with 4 class variables. See comments in dedth2v 2444.
|- (A = if(ph, A, R) -> (ps <-> ch))   &   |- (B = if(ph, B, S) -> (ch <-> th))   &   |- (C = if(ph, C, T) -> (th <-> ta))   &   |- (D = if(ph, D, U) -> (ta <-> et))   &   |- et   =>   |- (ph -> ps)
Theorem	dedth2h 2441	Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v 2444 but requires that each hypothesis has exactly one class variable. See also comments in dedth 2437.
|- (A = if(ph, A, C) -> (ch <-> th))   &   |- (B = if(ps, B, D) -> (th <-> ta))   &   |- ta   =>   |- ((ph /\ ps) -> ch)
Theorem	dedth3h 2442	Weak deduction theorem eliminating three hypotheses. See comments in dedth2h 2441.
|- (A = if(ph, A, D) -> (th <-> ta))   &   |- (B = if(ps, B, R) -> (ta <-> et))   &   |- (C = if(ch, C, S) -> (et <-> ze))   &   |- ze   =>   |- ((ph /\ ps /\ ch) -> th)
Theorem	dedth4h 2443	Weak deduction theorem eliminating four hypotheses. See comments in dedth2h 2441.
|- (A = if(ph, A, R) -> (ta <-> et))   &   |- (B = if(ps, B, S) -> (et <-> ze))   &   |- (C = if(ch, C, F) -> (ze <-> si))   &   |- (D = if(th, D, G) -> (si <-> rh))   &   |- rh   =>   |- (((ph /\ ps) /\ (ch /\ th)) -> ta)
Theorem	dedth2v 2444	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 2441 is simpler to use. See also comments in dedth 2437. (The proof was shortened by Eric Schmidt, 28-Jul-2009. Compare dedth2vOLD 2438. )
|- (A = if(ph, A, C) -> (ps <-> ch))   &   |- (B = if(ph, B, D) -> (ch <-> th))   &   |- th   =>   |- (ph -> ps)
Theorem	dedth3v 2445	Weak deduction theorem for eliminating a hypothesis with 3 class variables. See comments in dedth2v 2444. (The proof was shortened by Eric Schmidt, 28-Jul-2009. Compare dedth3vOLD 2439.)
|- (A = if(ph, A, D) -> (ps <-> ch))   &   |- (B = if(ph, B, R) -> (ch <-> th))   &   |- (C = if(ph, C, S) -> (th <-> ta))   &   |- ta   =>   |- (ph -> ps)
Theorem	dedth4v 2446	Weak deduction theorem for eliminating a hypothesis with 4 class variables. See comments in dedth2v 2444. (The proof was shortened by Eric Schmidt, 28-Jul-2009. Compare dedth4vOLD 2440.)
|- (A = if(ph, A, R) -> (ps <-> ch))   &   |- (B = if(ph, B, S) -> (ch <-> th))   &   |- (C = if(ph, C, T) -> (th <-> ta))   &   |- (D = if(ph, D, U) -> (ta <-> et))   &   |- et   =>   |- (ph -> ps)
Theorem	elimhyp 2447	Eliminate a hypothesis containing class variable A when it is known for a specific class B. For more information, see comments in dedth 2437.
|- (A = if(ph, A, B) -> (ph <-> ps))   &   |- (B = if(ph, A, B) -> (ch <-> ps))   &   |- ch   =>   |- ps
Theorem	elimhyp2v 2448	Eliminate a hypothesis containing 2 class variables.
|- (A = if(ph, A, C) -> (ph <-> ch))   &   |- (B = if(ph, B, D) -> (ch <-> th))   &   |- (C = if(ph, A, C) -> (ta <-> et))   &   |- (D = if(ph, B, D) -> (et <-> th))   &   |- ta   =>   |- th
Theorem	elimhyp3v 2449	Eliminate a hypothesis containing 3 class variables.
|- (A = if(ph, A, D) -> (ph <-> ch))   &   |- (B = if(ph, B, R) -> (ch <-> th))   &   |- (C = if(ph, C, S) -> (th <-> ta))   &   |- (D = if(ph, A, D) -> (et <-> ze))   &   |- (R = if(ph, B, R) -> (ze <-> si))   &   |- (S = if(ph, C, S) -> (si <-> ta))   &   |- et   =>   |- ta
Theorem	elimhyp4v 2450	Eliminate a hypothesis containing 4 class variables (for use with the weak deduction theorem dedth 2437).
|- (A = if(ph, A, D) -> (ph <-> ch))   &   |- (B = if(ph, B, R) -> (ch <-> th))   &   |- (C = if(ph, C, S) -> (th <-> ta))   &   |- (F = if(ph, F, G) -> (ta <-> ps))   &   |- (D = if(ph, A, D) -> (et <-> ze))   &   |- (R = if(ph, B, R) -> (ze <-> si))   &   |- (S = if(ph, C, S) -> (si <-> rh))   &   |- (G = if(ph, F, G) -> (rh <-> ps))   &   |- et   =>   |- ps
Theorem	elimel 2451	Eliminate a membership hypothesis for weak deduction theorem, when special case B e. C is provable.
|- B e. C   =>   |- if(A e. C, A, B) e. C
Theorem	elimdhyp 2452	Version of elimhyp 2447 where the hypothesis is deduced from the final antecedent. See ghomgrplem 10674 for an example of its use. (Contributed by Paul Chapman, 25-Mar-2008.)
|- (ph -> ps)   &   |- (A = if(ph, A, B) -> (ps <-> ch))   &   |- (B = if(ph, A, B) -> (th <-> ch))   &   |- th   =>   |- ch
Theorem	keephyp 2453	Transform a hypothesis ps 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(ph, A, B) -> (ps <-> th))   &   |- (B = if(ph, A, B) -> (ch <-> th))   &   |- ps   &   |- ch   =>   |- th
Theorem	keephyp2v 2454	Keep a hypothesis containing 2 class variables (for use with the weak deduction theorem dedth 2437).
|- (A = if(ph, A, C) -> (ps <-> ch))   &   |- (B = if(ph, B, D) -> (ch <-> th))   &   |- (C = if(ph, A, C) -> (ta <-> et))   &   |- (D = if(ph, B, D) -> (et <-> th))   &   |- ps   &   |- ta   =>   |- th
Theorem	keephyp3v 2455	Keep a hypothesis containing 3 class variables.
|- (A = if(ph, A, D) -> (rh <-> ch))   &   |- (B = if(ph, B, R) -> (ch <-> th))   &   |- (C = if(ph, C, S) -> (th <-> ta))   &   |- (D = if(ph, A, D) -> (et <-> ze))   &   |- (R = if(ph, B, R) -> (ze <-> si))   &   |- (S = if(ph, C, S) -> (si <-> ta))   &   |- rh   &   |- et   =>   |- ta
Theorem	keepel 2456	Keep a membership hypothesis for weak deduction theorem, when special case B e. C is provable.
|- A e. C   &   |- B e. C   =>   |- if(ph, A, B) e. C
Theorem	ifex 2457	Conditional operator existence.
|- A e. V   &   |- B e. V   =>   |- if(ph, A, B) e. V
Power classes
Syntax	cpw 2458	Extend class notation to include power class. (The tilde in the Metamath token is meant to suggest the calligraphic font of the P.)
class P~A
Definition	df-pw 2459	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.
|- P~A = {x | x (_ A}
Theorem	pweq 2460	Equality theorem for the power class.
|- (A = B -> P~A = P~B)
Theorem	elpw 2461	Membership in a power class. Theorem 86 of [Suppes] p. 47.
|- A e. V   =>   |- (A e. P~B <-> A (_ B)
Theorem	elpwg 2462	Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 2801.
|- (A e. C -> (A e. P~B <-> A (_ B))
Theorem	elpwi 2463	Subset relation implied by membership in a power class.
|- (A e. P~B -> A (_ B)
Theorem	hbpw 2464	Bound-variable hypothesis builder for power class.
|- (y e. A -> A.x y e. A)   =>   |- (y e. P~A -> A.x y e. P~A)
Theorem	pwid 2465	A set is a member of its power class. Theorem 87 of [Suppes] p. 47.
|- A e. V   =>   |- A e. P~A
Theorem	pwss 2466	Subclass relationship for power class.
|- (P~A (_ B <-> A.x(x (_ A -> x e. B))
Unordered and ordered pairs
Syntax	csn 2467	Extend class notation to include singleton.
class {A}
Syntax	cpr 2468	Extend class notation to include unordered pair.
class {A, B}
Syntax	cop 2469	Extend class notation to include ordered pair.
class <.A, B>.
Definition	df-sn 2470	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, although it is not very meaningful in this case. For an alternate definition see dfsn2 2478.
|- {A} = {x | x = A}
Definition	df-pr 2471	Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For a more traditional definition, but requiring a dummy variable, see dfpr2 2480.
|- {A, B} = ({A} u. {B})
Syntax	ctp 2472	Extend class notation to include unordered triplet.
class {A, B, C}
Definition	df-tp 2473	Define unordered triple of classes. Definition of [Enderton] p. 19.
|- {A, B, C} = ({A, B} u. {C})
Definition	df-op 2474	Kuratowski's ordered pair definition. Definition 9.1 of [Quine] p. 58. For proper classes it is not meaningful but is well-defined and we allow it for convenience (see opprc1 2563, opprc1b 2872, opprc2 2564, and opprc3 2873). For the justifying theorem (for sets) see opth 2863. 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 <.A, B>.2 = {{{A}, (/)}, {{B}}}, justified by opthwiener 2884, which was simplified by Kazimierz Kuratowski in 1921 to our present definition. An even simpler definition <.A, B>.3 = {A, {A, B}} is justified by opthreg 4749, but it requires the Axiom of Regularity for its justification and is not commonly used. A definition that also works for proper classes is <.A, B>.4 = ((A X. {(/)}) u. (B X. {{(/)}})), justified by opthprc 3306. If we restrict our sets to nonnegative integers, an ordered pair definition that involves only elementary arithmetic is provided by nn0opthi 6867. Finally, an ordered pair of real numbers can be represented by a complex number as shown by crui 6938.
|- <.A, B>. = {{A}, {A, B}}
Theorem	sneq 2475	Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15.
|- (A = B -> {A} = {B})
Theorem	sneqi 2476	Equality inference for singletons.
|- A = B   =>   |- {A} = {B}
Theorem	sneqd 2477	Equality deduction for singletons.
|- (ph -> A = B)   =>   |- (ph -> {A} = {B})
Theorem	dfsn2 2478	Alternate definition of singleton. Definition 5.1 of [TakeutiZaring] p. 15.
|- {A} = {A, A}
Theorem	elsn 2479	There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15.
|- (x e. {A} <-> x = A)
Theorem	dfpr2 2480	Alternate definition of unordered pair. Definition 5.1 of [TakeutiZaring] p. 15.
|- {A, B} = {x | (x = A \/ x = B)}
Theorem	elprg 2481	A member of an unordered pair of classes is one or the other of them. Exercise 1 of [TakeutiZaring] p. 15, generalized.
|- (A e. D -> (A e. {B, C} <-> (A = B \/ A = C)))
Theorem	elpr 2482	A member of an unordered pair of classes is one or the other of them. Exercise 1 of [TakeutiZaring] p. 15.
|- A e. V   =>   |- (A e. {B, C} <-> (A = B \/ A = C))
Theorem	elpr2 2483	A member of an unordered pair of classes is one or the other of them. Exercise 1 of [TakeutiZaring] p. 15.
|- B e. V   &   |- C e. V   =>   |- (A e. {B, C} <-> (A = B \/ A = C))
Theorem	hbpr 2484	Bound-variable hypothesis builder for unordered pairs.
|- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   =>   |- (y e. {A, B} -> A.x y e. {A, B})
Theorem	ifpr 2485	Membership of a conditional operator in an unordered pair.
|- ((A e. C /\ B e. D) -> if(ph, A, B) e. {A, B})
Theorem	ralpr 2486	Convert a quantification over a pair to a conjunction.
|- A e. V   &   |- B e. V   =>   |- (A.x e. {A, B}ph <-> ([A / x]ph /\ [B / x]ph))
Theorem	rexpr 2487	Convert an existential quantification over a pair to a disjunction.
|- A e. V   &   |- B e. V   =>   |- (E.x e. {A, B}ph <-> ([A / x]ph \/ [B / x]ph))
Theorem	ralsn 2488	Convert a quantification over a singleton to a substitution.
|- A e. V   =>   |- (A.x e. {A}ph <-> [A / x]ph)
Theorem	ralsng 2489	Substitution expressed in terms of quantification over a singleton.
|- (A e. B -> (A.x e. {A}ph <-> [A / x]ph))
Theorem	sbcsng 2490	Substitution expressed in terms of quantification over a singleton.
|- (A e. B -> ([A / x]ph <-> A.x e. {A}ph))
Theorem	elsncg 2491	There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15 (generalized).
|- (A e. C -> (A e. {B} <-> A = B))
Theorem	elsnc 2492	There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15.
|- A e. V   =>   |- (A e. {B} <-> A = B)
Theorem	elsni 2493	There is only one element in a singleton.
|- (A e. {B} -> A = B)
Theorem	snidg 2494	A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49.
|- (A e. B -> A e. {A})
Theorem	snidb 2495	A class is a set iff it is a member of its singleton.
|- (A e. V <-> A e. {A})
Theorem	snid 2496	A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49.
|- A e. V   =>   |- A e. {A}
Theorem	elsnc2g 2497	There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. This variation requires only that B, rather than A, be a set.
|- (B e. C -> (A e. {B} <-> A = B))
Theorem	elsnc2 2498	There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. This variation requires only that B, rather than A, be a set.
|- B e. V   =>   |- (A e. {B} <-> A = B)
Theorem	hbsn 2499	Bound-variable hypothesis builder for singletons.
|- (y e. A -> A.x y e. A)   =>   |- (y e. {A} -> A.x y e. {A})
Theorem	eltp 2500	A member of an unordered triple of classes is one of them. Special case of Exercise 1 of [TakeutiZaring] p. 17.
|- A e. V   =>   |- (A e. {B, C, D} <-> (A = B \/ A = C \/ A = D))