P. 326 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32501-32600   *Has distinct variable group(s)

Type	Label	Description
Statement
21.21  Mathbox for Norm Megill Note: A label suffixed with "N" (after the "Atoms..." section below), such as lshpnel2N 32597, means that the definition or theorem is not used for the derivation of hlathil 35578. This is a temporary renaming to assist cleaning up the theorems needed by hlathil 35578.
21.21.1  Obsolete schemes ax-c4,c5,c7,c10,c11,c11n,c15,c9,c14,c16 These older axiom schemes are obsolete and should not be used outside of this section. They are proved above as theorems axc4 , sp 1948, axc7 1950, axc10 2107, axc11 2159, axc11n 2154, axc15 2188, axc9 2151, axc14 2212, and axc16 2035.
Axiom	ax-c5 32501	Axiom of Specialization. A quantified wff implies the wff without a quantifier (i.e. an instance, or special case, of the generalized wff). In other words if something is true for all x, it is true for any specific x (that would typically occur as a free variable in the wff substituted for ph). (A free variable is one that does not occur in the scope of a quantifier: x and y are both free in x = y, but only x is free in A. y x = y.) Axiom scheme C5' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Axiom B5 of [Tarski] p. 67 (under his system S2, defined in the last paragraph on p. 77). Note that the converse of this axiom does not hold in general, but a weaker inference form of the converse holds and is expressed as rule ax-gen 1680. Conditional forms of the converse are given by ax-13 2102, ax-c14 32509, ax-c16 32510, and ax-5 1769. Unlike the more general textbook Axiom of Specialization, we cannot choose a variable different from x for the special case. For use, that requires the assistance of equality axioms, and we deal with it later after we introduce the definition of proper substitution - see stdpc4 2195. An interesting alternate axiomatization uses axc5c711 32535 and ax-c4 32502 in place of ax-c5 32501, ax-4 1693, ax-10 1926, and ax-11 1931. This axiom is obsolete and should no longer be used. It is proved above as theorem sp 1948. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.)
|- ( A. x ph -> ph )
Axiom	ax-c4 32502	Axiom of Quantified Implication. This axiom moves a quantifier from outside to inside an implication, quantifying ps. Notice that x must not be a free variable in the antecedent of the quantified implication, and we express this by binding ph to "protect" the axiom from a ph containing a free x. Axiom scheme C4' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Lemma 5 of [Monk2] p. 108 and Axiom 5 of [Mendelson] p. 69. This axiom is obsolete and should no longer be used. It is proved above as theorem axc4 1949. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.)
|- ( A. x ( A. x ph -> ps ) -> ( A. x ph -> A. x ps ) )
Axiom	ax-c7 32503	Axiom of Quantified Negation. This axiom is used to manipulate negated quantifiers. Equivalent to axiom scheme C7' in [Megill] p. 448 (p. 16 of the preprint). An alternate axiomatization could use axc5c711 32535 in place of ax-c5 32501, ax-c7 32503, and ax-11 1931. This axiom is obsolete and should no longer be used. It is proved above as theorem axc7 1950. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
|- ( -. A. x -. A. x ph -> ph )
Axiom	ax-c10 32504	A variant of ax6 2106. Axiom scheme C10' in [Megill] p. 448 (p. 16 of the preprint). This axiom is obsolete and should no longer be used. It is proved above as theorem axc10 2107. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
|- ( A. x ( x = y -> A. x ph ) -> ph )
Axiom	ax-c11 32505	Axiom ax-c11 32505 was the original version of ax-c11n 32506 ("n" for "new"), before it was discovered (in May 2008) that the shorter ax-c11n 32506 could replace it. It appears as Axiom scheme C11' in [Megill] p. 448 (p. 16 of the preprint). This axiom is obsolete and should no longer be used. It is proved above as theorem axc11 2159. (Contributed by NM, 10-May-1993.) (New usage is discouraged.)
|- ( A. x x = y -> ( A. x ph -> A. y ph ) )
Axiom	ax-c11n 32506	Axiom of Quantifier Substitution. One of the equality and substitution axioms of predicate calculus with equality. Appears as Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). The original version of this axiom was ax-c11 32505 and was replaced with this shorter ax-c11n 32506 ("n" for "new") in May 2008. The old axiom is proved from this one as theorem axc11 2159. Conversely, this axiom is proved from ax-c11 32505 as theorem axc11nfromc11 32543. This axiom was proved redundant in July 2015. See theorem axc11n 2154. This axiom is obsolete and should no longer be used. It is proved above as theorem axc11n 2154. (Contributed by NM, 16-May-2008.) (New usage is discouraged.)
|- ( A. x x = y -> A. y y = x )
Axiom	ax-c15 32507	Axiom ax-c15 32507 was the original version of ax-12 1944, before it was discovered (in Jan. 2007) that the shorter ax-12 1944 could replace it. It appears as Axiom scheme C15' in [Megill] p. 448 (p. 16 of the preprint). It is based on Lemma 16 of [Tarski] p. 70 and Axiom C8 of [Monk2] p. 105, from which it can be proved by cases. To understand this theorem more easily, think of " -. A. x x = y ->..." as informally meaning "if x and y are distinct variables then..." The antecedent becomes false if the same variable is substituted for x and y, ensuring the theorem is sound whenever this is the case. In some later theorems, we call an antecedent of the form -. A. x x = y a "distinctor." Interestingly, if the wff expression substituted for ph contains no wff variables, the resulting statement can be proved without invoking this axiom. This means that even though this axiom is metalogically independent from the others, it is not logically independent. Specifically, we can prove any wff-variable-free instance of axiom ax-c15 32507 (from which the ax-12 1944 instance follows by theorem ax12 32521.) The proof is by induction on formula length, using ax12eq 32558 and ax12el 32559 for the basis steps and ax12indn 32560, ax12indi 32561, and ax12inda 32565 for the induction steps. (This paragraph is true provided we use ax-c11 32505 in place of ax-c11n 32506.) This axiom is obsolete and should no longer be used. It is proved above as theorem axc15 2188, which should be used instead. (Contributed by NM, 14-May-1993.) (New usage is discouraged.)
|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
Axiom	ax-c9 32508	Axiom of Quantifier Introduction. One of the equality and substitution axioms of predicate calculus with equality. Informally, it says that whenever z is distinct from x and y, and x = y is true, then x = y quantified with z is also true. In other words, z is irrelevant to the truth of x = y. Axiom scheme C9' in [Megill] p. 448 (p. 16 of the preprint). It apparently does not otherwise appear in the literature but is easily proved from textbook predicate calculus by cases. This axiom is obsolete and should no longer be used. It is proved above as theorem axc9 2151. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
|- ( -. A. z z = x -> ( -. A. z z = y -> ( x = y -> A. z x = y ) ) )
Axiom	ax-c14 32509	Axiom of Quantifier Introduction. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. Axiom scheme C14' in [Megill] p. 448 (p. 16 of the preprint). It is redundant if we include ax-5 1769; see theorem axc14 2212. Alternately, ax-5 1769 becomes unnecessary in principle with this axiom, but we lose the more powerful metalogic afforded by ax-5 1769. We retain ax-c14 32509 here to provide completeness for systems with the simpler metalogic that results from omitting ax-5 1769, which might be easier to study for some theoretical purposes. This axiom is obsolete and should no longer be used. It is proved above as theorem axc14 2212. (Contributed by NM, 24-Jun-1993.) (New usage is discouraged.)
|- ( -. A. z z = x -> ( -. A. z z = y -> ( x e. y -> A. z x e. y ) ) )
Axiom	ax-c16 32510*	Axiom of Distinct Variables. The only axiom of predicate calculus requiring that variables be distinct (if we consider ax-5 1769 to be a metatheorem and not an axiom). Axiom scheme C16' in [Megill] p. 448 (p. 16 of the preprint). It apparently does not otherwise appear in the literature but is easily proved from textbook predicate calculus by cases. It is a somewhat bizarre axiom since the antecedent is always false in set theory (see dtru 4611), but nonetheless it is technically necessary as you can see from its uses. This axiom is redundant if we include ax-5 1769; see theorem axc16 2035. Alternately, ax-5 1769 becomes logically redundant in the presence of this axiom, but without ax-5 1769 we lose the more powerful metalogic that results from being able to express the concept of a setvar variable not occurring in a wff (as opposed to just two setvar variables being distinct). We retain ax-c16 32510 here to provide logical completeness for systems with the simpler metalogic that results from omitting ax-5 1769, which might be easier to study for some theoretical purposes. This axiom is obsolete and should no longer be used. It is proved above as theorem axc16 2035. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
|- ( A. x x = y -> ( ph -> A. x ph ) )
21.21.2  Rederive new axioms from old: ax4 , ax10 , ax6fromc10 , ax12 , ax13fromc9 Theorems ax12 32521 and ax13fromc9 32522 require some intermediate theorems that are included in this section.
Theorem	axc5 32511	This theorem repeats sp 1948 under the name axc5 32511, so that the metamath program's "verify markup" command will check that it matches axiom scheme ax-c5 32501. It is preferred that references to this theorem use the name sp 1948. (Contributed by NM, 18-Aug-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A. x ph -> ph )
Theorem	ax4 32512	Rederivation of axiom ax-4 1693 from ax-c4 32502 and other older axioms. See axc4 1949 for the derivation of ax-c4 32502 from ax-4 1693. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
Theorem	ax10 32513	Rederivation of axiom ax-10 1926 from ax-c7 32503 and other older axioms. See axc7 1950 for the derivation of ax-c7 32503 from ax-10 1926. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x ph -> A. x -. A. x ph )
Theorem	ax6fromc10 32514	Rederivation of axiom ax-6 1816 from ax-c10 32504 and other older axioms. See axc10 2107 for the derivation of ax-c10 32504 from ax-6 1816. Lemma L18 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
|- -. A. x -. x = y
Theorem	hba1-o 32515	x is not free in A. x ph. Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114. (Contributed by NM, 24-Jan-1993.) (New usage is discouraged.)
|- ( A. x ph -> A. x A. x ph )
Theorem	axc4i-o 32516	Inference version of ax-c4 32502. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.)
|- ( A. x ph -> ps )   =>    |- ( A. x ph -> A. x ps )
Theorem	aecom-o 32517	Commutation law for identical variable specifiers. The antecedent and consequent are true when x and y are substituted with the same variable. Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). Version of aecom 2156 using ax-c11 32505. Unlike axc11nfromc11 32543, this version does not require ax-5 1769. (Contributed by NM, 10-May-1993.) (New usage is discouraged.)
|- ( A. x x = y -> A. y y = x )
Theorem	aecoms-o 32518	A commutation rule for identical variable specifiers. Version of aecoms 2157 using ax-c11 . (Contributed by NM, 10-May-1993.) (New usage is discouraged.)
|- ( A. x x = y -> ph )   =>    |- ( A. y y = x -> ph )
Theorem	hbae-o 32519	All variables are effectively bound in an identical variable specifier. Version of hbae 2160 using ax-c11 32505. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x x = y -> A. z A. x x = y )
Theorem	dral1-o 32520	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Version of dral1 2170 using ax-c11 32505. (Contributed by NM, 24-Nov-1994.) (New usage is discouraged.)
|- ( A. x x = y -> ( ph <-> ps ) )   =>    |- ( A. x x = y -> ( A. x ph <-> A. y ps ) )
Theorem	ax12 32521	Rederivation of axiom ax-12 1944 from ax-c15 32507, ax-c11 32505, and other older axioms. See theorem axc15 2188 for the derivation of ax-c15 32507 from ax-12 1944. An open problem is whether we can prove this using ax-c11n 32506 instead of ax-c11 32505. This proof uses newer axioms ax-4 1693 and ax-6 1816, but since these are proved from the older axioms above, this is acceptable and lets us avoid having to reprove several earlier theorems to use ax-c4 32502 and ax-c10 32504. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )
Theorem	ax13fromc9 32522	Derive ax-13 2102 from ax-c9 32508 and other older axioms. This proof uses newer axioms ax-4 1693 and ax-6 1816, but since these are proved from the older axioms above, this is acceptable and lets us avoid having to reprove several earlier theorems to use ax-c4 32502 and ax-c10 32504. (Contributed by NM, 21-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. x = y -> ( y = z -> A. x y = z ) )
21.21.3  Legacy theorems using obsolete axioms These theorems were mostly intended to study properties of the older axiom schemes and are not useful outside of this section. They should not be used outside of this section. They may be deleted when they are deemed to no longer be of interest.
Theorem	ax5ALT 32523*	Axiom to quantify a variable over a formula in which it does not occur. Axiom C5 in [Megill] p. 444 (p. 11 of the preprint). Also appears as Axiom B6 (p. 75) of system S2 of [Tarski] p. 77 and Axiom C5-1 of [Monk2] p. 113. (This theorem simply repeats ax-5 1769 so that we can include the following note, which applies only to the obsolete axiomatization.) This axiom is logically redundant in the (logically complete) predicate calculus axiom system consisting of ax-gen 1680, ax-c4 32502, ax-c5 32501, ax-11 1931, ax-c7 32503, ax-7 1862, ax-c9 32508, ax-c10 32504, ax-c11 32505, ax-8 1900, ax-9 1907, ax-c14 32509, ax-c15 32507, and ax-c16 32510: in that system, we can derive any instance of ax-5 1769 not containing wff variables by induction on formula length, using ax5eq 32549 and ax5el 32554 for the basis together hbn 1988, hbal 1933, and hbim 2016. However, if we omit this axiom, our development would be quite inconvenient since we could work only with specific instances of wffs containing no wff variables - this axiom introduces the concept of a setvar variable not occurring in a wff (as opposed to just two setvar variables being distinct). (Contributed by NM, 19-Aug-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> A. x ph )
Theorem	equid1 32524	Proof of equid 1866 from our older axioms. This is often an axiom of equality in textbook systems, but we don't need it as an axiom since it can be proved from our other axioms (although the proof, as you can see below, is not as obvious as you might think). This proof uses only axioms without distinct variable conditions and requires no dummy variables. A simpler proof, similar to Tarski's, is possible if we make use of ax-5 1769; see the proof of equid 1866. See equid1ALT 32542 for an alternate proof. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
|- x = x
Theorem	sps-o 32525	Generalization of antecedent. (Contributed by NM, 5-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ps )   =>    |- ( A. x ph -> ps )
Theorem	hbequid 32526	Bound-variable hypothesis builder for x = x. This theorem tells us that any variable, including x, is effectively not free in x = x, even though x is technically free according to the traditional definition of free variable. (The proof does not use ax-c10 32504.) (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 23-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( x = x -> A. y x = x )
Theorem	nfequid-o 32527	Bound-variable hypothesis builder for x = x. This theorem tells us that any variable, including x, is effectively not free in x = x, even though x is technically free according to the traditional definition of free variable. (The proof uses only ax-4 1693, ax-7 1862, ax-c9 32508, and ax-gen 1680. This shows that this can be proved without ax6 2106, even though the theorem equid 1866 cannot be. A shorter proof using ax6 2106 is obtainable from equid 1866 and hbth 1686.) Remark added 2-Dec-2015 NM: This proof does implicitly use ax6v 1817, which is used for the derivation of axc9 2151, unless we consider ax-c9 32508 the starting axiom rather than ax-13 2102. (Contributed by NM, 13-Jan-2011.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ y x = x
Theorem	axc5c7 32528	Proof of a single axiom that can replace ax-c5 32501 and ax-c7 32503. See axc5c7toc5 32529 and axc5c7toc7 32530 for the re-derivation of those axioms. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( A. x -. A. x ph -> A. x ph ) -> ph )
Theorem	axc5c7toc5 32529	Re-derivation of ax-c5 32501 from axc5c7 32528. Only propositional calculus is used for the re-derivation. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x ph -> ph )
Theorem	axc5c7toc7 32530	Re-derivation of ax-c7 32503 from axc5c7 32528. Only propositional calculus is used for the re-derivation. (Contributed by Scott Fenton, 12-Sep-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x -. A. x ph -> ph )
Theorem	axc711 32531	Proof of a single axiom that can replace both ax-c7 32503 and ax-11 1931. See axc711toc7 32533 and axc711to11 32534 for the re-derivation of those axioms. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x -. A. y A. x ph -> A. y ph )
Theorem	nfa1-o 32532	x is not free in A. x ph. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x A. x ph
Theorem	axc711toc7 32533	Re-derivation of ax-c7 32503 from axc711 32531. Note that ax-c7 32503 and ax-11 1931 are not used by the re-derivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x -. A. x ph -> ph )
Theorem	axc711to11 32534	Re-derivation of ax-11 1931 from axc711 32531. Note that ax-c7 32503 and ax-11 1931 are not used by the re-derivation. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x A. y ph -> A. y A. x ph )
Theorem	axc5c711 32535	Proof of a single axiom that can replace ax-c5 32501, ax-c7 32503, and ax-11 1931 in a subsystem that includes these axioms plus ax-c4 32502 and ax-gen 1680 (and propositional calculus). See axc5c711toc5 32536, axc5c711toc7 32537, and axc5c711to11 32538 for the re-derivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 32528. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( A. x A. y -. A. x A. y ph -> A. x ph ) -> ph )
Theorem	axc5c711toc5 32536	Re-derivation of ax-c5 32501 from axc5c711 32535. Only propositional calculus is used by the re-derivation. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x ph -> ph )
Theorem	axc5c711toc7 32537	Re-derivation of ax-c7 32503 from axc5c711 32535. Note that ax-c7 32503 and ax-11 1931 are not used by the re-derivation. The use of alimi 1695 (which uses ax-c5 32501) is allowed since we have already proved axc5c711toc5 32536. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x -. A. x ph -> ph )
Theorem	axc5c711to11 32538	Re-derivation of ax-11 1931 from axc5c711 32535. Note that ax-c7 32503 and ax-11 1931 are not used by the re-derivation. The use of alimi 1695 (which uses ax-c5 32501) is allowed since we have already proved axc5c711toc5 32536. (Contributed by NM, 19-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x A. y ph -> A. y A. x ph )
Theorem	equidqe 32539	equid 1866 with existential quantifier without using ax-c5 32501 or ax-5 1769. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
|- -. A. y -. x = x
Theorem	axc5sp1 32540	A special case of ax-c5 32501 without using ax-c5 32501 or ax-5 1769. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. y -. x = x -> -. x = x )
Theorem	equidq 32541	equid 1866 with universal quantifier without using ax-c5 32501 or ax-5 1769. (Contributed by NM, 13-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- A. y x = x
Theorem	equid1ALT 32542	Alternate proof of equid 1866 and equid1 32524 from older axioms ax-c7 32503, ax-c10 32504 and ax-c9 32508. (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
|- x = x
Theorem	axc11nfromc11 32543	Rederivation of ax-c11n 32506 from original version ax-c11 32505. See theorem axc11 2159 for the derivation of ax-c11 32505 from ax-c11n 32506. This theorem should not be referenced in any proof. Instead, use ax-c11n 32506 above so that uses of ax-c11n 32506 can be more easily identified, or use aecom-o 32517 when this form is needed for studies involving ax-c11 32505 and omitting ax-5 1769. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x x = y -> A. y y = x )
Theorem	naecoms-o 32544	A commutation rule for distinct variable specifiers. Version of naecoms 2158 using ax-c11 32505. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x x = y -> ph )   =>    |- ( -. A. y y = x -> ph )
Theorem	hbnae-o 32545	All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). Version of hbnae 2162 using ax-c11 32505. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x x = y -> A. z -. A. x x = y )
Theorem	dvelimf-o 32546	Proof of dvelimh 2181 that uses ax-c11 32505 but not ax-c15 32507, ax-c11n 32506, or ax-12 1944. Version of dvelimh 2181 using ax-c11 32505 instead of axc11 2159. (Contributed by NM, 12-Nov-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. z ps )   &    |- ( z = y -> ( ph <-> ps ) )   =>    |- ( -. A. x x = y -> ( ps -> A. x ps ) )
Theorem	dral2-o 32547	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Version of dral2 2169 using ax-c11 32505. (Contributed by NM, 27-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x x = y -> ( ph <-> ps ) )   =>    |- ( A. x x = y -> ( A. z ph <-> A. z ps ) )
Theorem	aev-o 32548*	A "distinctor elimination" lemma with no restrictions on variables in the consequent, proved without using ax-c16 32510. Version of aev 2037 using ax-c11 32505. (Contributed by NM, 8-Nov-2006.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x x = y -> A. z w = v )
Theorem	ax5eq 32549*	Theorem to add distinct quantifier to atomic formula. (This theorem demonstrates the induction basis for ax-5 1769 considered as a metatheorem. Do not use it for later proofs - use ax-5 1769 instead, to avoid reference to the redundant axiom ax-c16 32510.) (Contributed by NM, 10-Jan-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( x = y -> A. z x = y )
Theorem	dveeq2-o 32550*	Quantifier introduction when one pair of variables is distinct. Version of dveeq2 2147 using ax-c15 32507. (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x x = y -> ( z = y -> A. x z = y ) )
Theorem	axc16g-o 32551*	A generalization of axiom ax-c16 32510. Version of axc16g 2034 using ax-c11 32505. (Contributed by NM, 15-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x x = y -> ( ph -> A. z ph ) )
Theorem	dveeq1-o 32552*	Quantifier introduction when one pair of variables is distinct. Version of dveeq1 2149 using ax-c11 . (Contributed by NM, 2-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x x = y -> ( y = z -> A. x y = z ) )
Theorem	dveeq1-o16 32553*	Version of dveeq1 2149 using ax-c16 32510 instead of ax-5 1769. (Contributed by NM, 29-Apr-2008.) TODO: Recover proof from older set.mm to remove use of ax-5 1769. (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x x = y -> ( y = z -> A. x y = z ) )
Theorem	ax5el 32554*	Theorem to add distinct quantifier to atomic formula. This theorem demonstrates the induction basis for ax-5 1769 considered as a metatheorem.) (Contributed by NM, 22-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( x e. y -> A. z x e. y )
Theorem	axc11n-16 32555*	This theorem shows that, given ax-c16 32510, we can derive a version of ax-c11n 32506. However, it is weaker than ax-c11n 32506 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 27-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x x = z -> A. z z = x )
Theorem	dveel2ALT 32556*	Alternate proof of dveel2 2211 using ax-c16 32510 instead of ax-5 1769. (Contributed by NM, 10-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x x = y -> ( z e. y -> A. x z e. y ) )
Theorem	ax12f 32557	Basis step for constructing a substitution instance of ax-c15 32507 without using ax-c15 32507. We can start with any formula ph in which x is not free. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> A. x ph )   =>    |- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
Theorem	ax12eq 32558	Basis step for constructing a substitution instance of ax-c15 32507 without using ax-c15 32507. Atomic formula for equality predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x x = y -> ( x = y -> ( z = w -> A. x ( x = y -> z = w ) ) ) )
Theorem	ax12el 32559	Basis step for constructing a substitution instance of ax-c15 32507 without using ax-c15 32507. Atomic formula for membership predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x x = y -> ( x = y -> ( z e. w -> A. x ( x = y -> z e. w ) ) ) )
Theorem	ax12indn 32560	Induction step for constructing a substitution instance of ax-c15 32507 without using ax-c15 32507. Negation case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )   =>    |- ( -. A. x x = y -> ( x = y -> ( -. ph -> A. x ( x = y -> -. ph ) ) ) )
Theorem	ax12indi 32561	Induction step for constructing a substitution instance of ax-c15 32507 without using ax-c15 32507. Implication case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )   &    |- ( -. A. x x = y -> ( x = y -> ( ps -> A. x ( x = y -> ps ) ) ) )   =>    |- ( -. A. x x = y -> ( x = y -> ( ( ph -> ps ) -> A. x ( x = y -> ( ph -> ps ) ) ) ) )
Theorem	ax12indalem 32562	Lemma for ax12inda2 32564 and ax12inda 32565. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )   =>    |- ( -. A. y y = z -> ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) )
Theorem	ax12inda2ALT 32563*	Alternate proof of ax12inda2 32564, slightly more direct and not requiring ax-c16 32510. (Contributed by NM, 4-May-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )   =>    |- ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) )
Theorem	ax12inda2 32564*	Induction step for constructing a substitution instance of ax-c15 32507 without using ax-c15 32507. Quantification case. When z and y are distinct, this theorem avoids the dummy variables needed by the more general ax12inda 32565. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )   =>    |- ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) )
Theorem	ax12inda 32565*	Induction step for constructing a substitution instance of ax-c15 32507 without using ax-c15 32507. Quantification case. (When z and y are distinct, ax12inda2 32564 may be used instead to avoid the dummy variable w in the proof.) (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x x = w -> ( x = w -> ( ph -> A. x ( x = w -> ph ) ) ) )   =>    |- ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) )
Theorem	ax12v2-o 32566*	Recovery of ax-c15 32507 from ax12v 1945 without using ax-c15 32507. The hypothesis is even weaker than ax12v 1945, with z both distinct from x and not occurring in ph. Thus, the hypothesis provides an alternate axiom that can be used in place of ax-c15 32507. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( x = z -> ( ph -> A. x ( x = z -> ph ) ) )   =>    |- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
Theorem	ax12a2-o 32567*	Derive ax-c15 32507 from a hypothesis in the form of ax-12 1944, without using ax-12 1944 or ax-c15 32507. The hypothesis is even weaker than ax-12 1944, with z both distinct from x and not occurring in ph. Thus, the hypothesis provides an alternate axiom that can be used in place of ax-12 1944, if we also hvae ax-c11 32505 which this proof uses . As theorem ax12 32521 shows, the distinct variable conditions are optional. An open problem is whether we can derive this with ax-c11n 32506 instead of ax-c11 32505. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( x = z -> ( A. z ph -> A. x ( x = z -> ph ) ) )   =>    |- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
Theorem	axc11-o 32568	Show that ax-c11 32505 can be derived from ax-c11n 32506. An open problem is whether this theorem can be derived from ax-c11n 32506 and the others when ax-12 1944 is replaced with ax-c15 32507. See theorem axc11nfromc11 32543 for the rederivation of ax-c11n 32506 from axc11 2159. Normally, axc11 2159 should be used rather than ax-c11 32505 or axc11-o 32568, except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x x = y -> ( A. x ph -> A. y ph ) )
Theorem	fsumshftd 32569*	Index shift of a finite sum with a weaker "implicit substitution" hypothesis than fsumshft 13896. The proof demonstrates how this can be derived starting from from fsumshft 13896. (Contributed by NM, 1-Nov-2019.)
|- ( ph -> K e. ZZ )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )   &    |- ( ( ph /\ j = ( k - K ) ) -> A = B )   =>    |- ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( M + K ) ... ( N + K ) ) B )
Theorem	fsumshftdOLD 32570*	Obsolete version of fsumshftd 32569 as of 1-Nov-2019. (Contributed by NM, 1-Nov-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> K e. ZZ )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )   &    |- ( ( ph /\ j = ( k - K ) ) -> A = B )   =>    |- ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( M + K ) ... ( N + K ) ) B )
Axiom	ax-riotaBAD 32571	Define restricted description binder. In case it doesn't exist, we return a set which is not a member of the domain of discourse A. See also comments for df-iota 5569. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) WARNING: THIS "AXIOM", WHICH IS THE OLD df-riota 6282, CONFLICTS WITH (THE NEW) df-riota 6282 AND MAKES THE SYSTEM IN set.mm INCONSISTENT. IT IS TEMPORARY AND WILL BE DELETED AFTER ALL USES ARE ELIMINATED.
|- ( iota_ x e. A ph ) = if ( E! x e. A ph , ( iota x ( x e. A /\ ph ) ) , ( Undef ` { x | x e. A } ) )
Theorem	riotaclbgBAD 32572*	Closure of restricted iota. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 24-Dec-2016.)
|- ( A e. V -> ( E! x e. A ph <-> ( iota_ x e. A ph ) e. A ) )
Theorem	riotaclbBAD 32573*	Closure of restricted iota. (Contributed by NM, 15-Sep-2011.)
|- A e. _V   =>    |- ( E! x e. A ph <-> ( iota_ x e. A ph ) e. A )
Theorem	riotasvd 32574*	Deduction version of riotasv 32577. (Contributed by NM, 4-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- ( ph -> D = ( iota_ x e. A A. y e. B ( ps -> x = C ) ) )   &    |- ( ph -> D e. A )   =>    |- ( ( ph /\ A e. V ) -> ( ( y e. B /\ ps ) -> D = C ) )
Theorem	riotasv2d 32575*	Value of description binder D for a single-valued class expression C ( y ) (as in e.g. reusv2 4626). Special case of riota2f 6303. (Contributed by NM, 2-Mar-2013.)
|- F/ y ph   &    |- ( ph -> F/_ y F )   &    |- ( ph -> F/ y ch )   &    |- ( ph -> D = ( iota_ x e. A A. y e. B ( ps -> x = C ) ) )   &    |- ( ( ph /\ y = E ) -> ( ps <-> ch ) )   &    |- ( ( ph /\ y = E ) -> C = F )   &    |- ( ph -> D e. A )   &    |- ( ph -> E e. B )   &    |- ( ph -> ch )   =>    |- ( ( ph /\ A e. V ) -> D = F )
Theorem	riotasv2s 32576*	The value of description binder D for a single-valued class expression C ( y ) (as in e.g. reusv2 4626) in the form of a substitution instance. Special case of riota2f 6303. (Contributed by NM, 3-Mar-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
|- D = ( iota_ x e. A A. y e. B ( ph -> x = C ) )   =>    |- ( ( A e. V /\ D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) -> D = [_ E / y ]_ C )
Theorem	riotasv 32577*	Value of description binder D for a single-valued class expression C ( y ) (as in e.g. reusv2 4626). Special case of riota2f 6303. (Contributed by NM, 26-Jan-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
|- A e. _V   &    |- D = ( iota_ x e. A A. y e. B ( ph -> x = C ) )   =>    |- ( ( D e. A /\ y e. B /\ ph ) -> D = C )
Theorem	riotasv3d 32578*	A property ch holding for a representative of a single-valued class expression C ( y ) (see e.g. reusv2 4626) also holds for its description binder D (in the form of property th). (Contributed by NM, 5-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/ y ph   &    |- ( ph -> F/ y th )   &    |- ( ph -> D = ( iota_ x e. A A. y e. B ( ps -> x = C ) ) )   &    |- ( ( ph /\ C = D ) -> ( ch <-> th ) )   &    |- ( ph -> ( ( y e. B /\ ps ) -> ch ) )   &    |- ( ph -> D e. A )   &    |- ( ph -> E. y e. B ps )   =>    |- ( ( ph /\ A e. V ) -> th )
21.21.4  Experiments with weak deduction theorem
Theorem	elimhyps 32579	A version of elimhyp 3951 using explicit substitution. (Contributed by NM, 15-Jun-2019.)
|- [. B / x ]. ph   =>    |- [. if ( ph , x , B ) / x ]. ph
Theorem	dedths 32580	A version of weak deduction theorem dedth 3944 using explicit substitution. (Contributed by NM, 15-Jun-2019.)
|- [. if ( ph , x , B ) / x ]. ps   =>    |- ( ph -> ps )
Theorem	renegclALT 32581	Closure law for negative of reals. Demonstrates use of weak deduction theorem with explicit substitution. The proof is much longer than that of renegcl 9968. (Contributed by NM, 15-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A e. RR -> -u A e. RR )
Theorem	elimhyps2 32582	Generalization of elimhyps 32579 that is not useful unless we can separately prove |- A e. _V. (Contributed by NM, 13-Jun-2019.)
|- [. B / x ]. ph   =>    |- [. if ( [. A / x ]. ph , A , B ) / x ]. ph
Theorem	dedths2 32583	Generalization of dedths 32580 that is not useful unless we can separately prove |- A e. _V. (Contributed by NM, 13-Jun-2019.)
|- [. if ( [. A / x ]. ph , A , B ) / x ]. ps   =>    |- ( [. A / x ]. ph -> [. A / x ]. ps )
21.21.5  Miscellanea
Theorem	cnaddcom 32584	Recover the commutative law of addition for complex numbers from the Abelian group structure. (Contributed by NM, 17-Mar-2013.) (Proof modification is discouraged.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
Theorem	toycom 32585*	Show the commutative law for an operation O on a toy structure class C of commuatitive operations on CC. This illustrates how a structure class can be partially specialized. In practice, we would ordinarily define a new constant such as "CAbel" in place of C. (Contributed by NM, 17-Mar-2013.) (Proof modification is discouraged.)
|- C = { g e. Abel | ( Base ` g ) = CC }   &    |- .+ = ( +g ` K )   =>    |- ( ( K e. C /\ A e. CC /\ B e. CC ) -> ( A .+ B ) = ( B .+ A ) )
21.21.6  Atoms, hyperplanes, and covering in a left vector space (or module)
Syntax	clsa 32586	Extend class notation with all 1-dim subspaces (atoms) of a left module or left vector space.
class LSAtoms
Syntax	clsh 32587	Extend class notation with all subspaces of a left module or left vector space that are hyperplanes.
class LSHyp
Definition	df-lsatoms 32588*	Define the set of all 1-dim subspaces (atoms) of a left module or left vector space. (Contributed by NM, 9-Apr-2014.)
|- LSAtoms = ( w e. _V |-> ran ( v e. ( ( Base ` w ) \ { ( 0g ` w ) } ) |-> ( ( LSpan ` w ) ` { v } ) ) )
Definition	df-lshyp 32589*	Define the set of all hyperplanes of a left module or left vector space. Also called co-atoms, these are subspaces that are one dimension less that the full space. (Contributed by NM, 29-Jun-2014.)
|- LSHyp = ( w e. _V |-> { s e. ( LSubSp ` w ) | ( s =/= ( Base ` w ) /\ E. v e. ( Base ` w ) ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) ) } )
Theorem	lshpset 32590*	The set of all hyperplanes of a left module or left vector space. The vector v is called a generating vector for the hyperplane. (Contributed by NM, 29-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- S = ( LSubSp ` W )   &    |- H = (LSHyp ` W )   =>    |- ( W e. X -> H = { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } )
Theorem	islshp 32591*	The predicate "is a hyperplane" (of a left module or left vector space). (Contributed by NM, 29-Jun-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- S = ( LSubSp ` W )   &    |- H = (LSHyp ` W )   =>    |- ( W e. X -> ( U e. H <-> ( U e. S /\ U =/= V /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) ) )
Theorem	islshpsm 32592*	Hyperplane properties expressed with subspace sum. (Contributed by NM, 3-Jul-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- S = ( LSubSp ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LMod )   =>    |- ( ph -> ( U e. H <-> ( U e. S /\ U =/= V /\ E. v e. V ( U .(+) ( N ` { v } ) ) = V ) ) )
Theorem	lshplss 32593	A hyperplane is a subspace. (Contributed by NM, 3-Jul-2014.)
|- S = ( LSubSp ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. H )   =>    |- ( ph -> U e. S )
Theorem	lshpne 32594	A hyperplane is not equal to the vector space. (Contributed by NM, 4-Jul-2014.)
|- V = ( Base ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. H )   =>    |- ( ph -> U =/= V )
Theorem	lshpnel 32595	A hyperplane's generating vector does not belong to the hyperplane. (Contributed by NM, 3-Jul-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. H )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { X } ) ) = V )   =>    |- ( ph -> -. X e. U )
Theorem	lshpnelb 32596	The subspace sum of a hyperplane and the span of an element equals the vector space iff the element is not in the hyperplane. (Contributed by NM, 2-Oct-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( -. X e. U <-> ( U .(+) ( N ` { X } ) ) = V ) )
Theorem	lshpnel2N 32597	Condition that determines a hyperplane. (Contributed by NM, 3-Oct-2014.) (New usage is discouraged.)
|- V = ( Base ` W )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. S )   &    |- ( ph -> U =/= V )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. U )   =>    |- ( ph -> ( U e. H <-> ( U .(+) ( N ` { X } ) ) = V ) )
Theorem	lshpne0 32598	The member of the span in the hyperplane definition does not belong to the hyperplane. (Contributed by NM, 14-Jul-2014.)
|- V = ( Base ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- .0. = ( 0g ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> U e. H )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { X } ) ) = V )   =>    |- ( ph -> X =/= .0. )
Theorem	lshpdisj 32599	A hyperplane and the span in the hyperplane definition are disjoint. (Contributed by NM, 3-Jul-2014.)
|- V = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- .(+) = ( LSSum ` W )   &    |- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> U e. H )   &    |- ( ph -> X e. V )   &    |- ( ph -> ( U .(+) ( N ` { X } ) ) = V )   =>    |- ( ph -> ( U i^i ( N ` { X } ) ) = { .0. } )
Theorem	lshpcmp 32600	If two hyperplanes are comparable, they are equal. (Contributed by NM, 9-Oct-2014.)
|- H = (LSHyp ` W )   &    |- ( ph -> W e. LVec )   &    |- ( ph -> T e. H )   &    |- ( ph -> U e. H )   =>    |- ( ph -> ( T C_ U <-> T = U ) )