mmtheorems10 - 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 - 901-1000 - Page 10 of 123

Type	Label	Description
Statement
Theorem	3anbi13d 901	Deduction conjoining and adding a conjunct to equivalences.
|- (ph -> (ps <-> ch))   &   |- (ph -> (th <-> ta))   =>   |- (ph -> ((ps /\ et /\ th) <-> (ch /\ et /\ ta)))
Theorem	3anbi23d 902	Deduction conjoining and adding a conjunct to equivalences.
|- (ph -> (ps <-> ch))   &   |- (ph -> (th <-> ta))   =>   |- (ph -> ((et /\ ps /\ th) <-> (et /\ ch /\ ta)))
Theorem	3anbi1d 903	Deduction adding conjuncts to an equivalence.
|- (ph -> (ps <-> ch))   =>   |- (ph -> ((ps /\ th /\ ta) <-> (ch /\ th /\ ta)))
Theorem	3anbi2d 904	Deduction adding conjuncts to an equivalence.
|- (ph -> (ps <-> ch))   =>   |- (ph -> ((th /\ ps /\ ta) <-> (th /\ ch /\ ta)))
Theorem	3anbi3d 905	Deduction adding conjuncts to an equivalence.
|- (ph -> (ps <-> ch))   =>   |- (ph -> ((th /\ ta /\ ps) <-> (th /\ ta /\ ch)))
Theorem	3anim123d 906	Deduction joining 3 implications to form implication of conjunctions.
|- (ph -> (ps -> ch))   &   |- (ph -> (th -> ta))   &   |- (ph -> (et -> ze))   =>   |- (ph -> ((ps /\ th /\ et) -> (ch /\ ta /\ ze)))
Theorem	3orim123d 907	Deduction joining 3 implications to form implication of disjunctions.
|- (ph -> (ps -> ch))   &   |- (ph -> (th -> ta))   &   |- (ph -> (et -> ze))   =>   |- (ph -> ((ps \/ th \/ et) -> (ch \/ ta \/ ze)))
Theorem	an6 908	Rearrangement of 6 conjuncts.
|- (((ph /\ ps /\ ch) /\ (th /\ ta /\ et)) <-> ((ph /\ th) /\ (ps /\ ta) /\ (ch /\ et)))
Theorem	mp3an1 909	An inference based on modus ponens.
|- ph   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- ((ps /\ ch) -> th)
Theorem	mp3an2 910	An inference based on modus ponens.
|- ps   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- ((ph /\ ch) -> th)
Theorem	mp3an3 911	An inference based on modus ponens.
|- ch   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- ((ph /\ ps) -> th)
Theorem	mp3an12 912	An inference based on modus ponens.
|- ph   &   |- ps   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- (ch -> th)
Theorem	mp3an13 913	An inference based on modus ponens.
|- ph   &   |- ch   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- (ps -> th)
Theorem	mp3an23 914	An inference based on modus ponens.
|- ps   &   |- ch   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- (ph -> th)
Theorem	mp3an1i 915	An inference based on modus ponens.
|- ps   &   |- (ph -> ((ps /\ ch /\ th) -> ta))   =>   |- (ph -> ((ch /\ th) -> ta))
Theorem	mp3anl1 916	An inference based on modus ponens.
|- ph   &   |- (((ph /\ ps /\ ch) /\ th) -> ta)   =>   |- (((ps /\ ch) /\ th) -> ta)
Theorem	mp3anl2 917	An inference based on modus ponens.
|- ps   &   |- (((ph /\ ps /\ ch) /\ th) -> ta)   =>   |- (((ph /\ ch) /\ th) -> ta)
Theorem	mp3anl3 918	An inference based on modus ponens.
|- ch   &   |- (((ph /\ ps /\ ch) /\ th) -> ta)   =>   |- (((ph /\ ps) /\ th) -> ta)
Theorem	mp3anr1 919	An inference based on modus ponens.
|- ps   &   |- ((ph /\ (ps /\ ch /\ th)) -> ta)   =>   |- ((ph /\ (ch /\ th)) -> ta)
Theorem	mp3anr2 920	An inference based on modus ponens.
|- ch   &   |- ((ph /\ (ps /\ ch /\ th)) -> ta)   =>   |- ((ph /\ (ps /\ th)) -> ta)
Theorem	mp3anr3 921	An inference based on modus ponens.
|- th   &   |- ((ph /\ (ps /\ ch /\ th)) -> ta)   =>   |- ((ph /\ (ps /\ ch)) -> ta)
Theorem	mp3an 922	An inference based on modus ponens.
|- ph   &   |- ps   &   |- ch   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- th
Theorem	mpd3an3 923	An inference based on modus ponens.
|- ((ph /\ ps) -> ch)   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- ((ph /\ ps) -> th)
Theorem	mpd3an23 924	An inference based on modus ponens.
|- (ph -> ps)   &   |- (ph -> ch)   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- (ph -> th)
Theorem	biimp3a 925	Infer implication from a logical equivalence. Similar to biimpa 416.
|- ((ph /\ ps) -> (ch <-> th))   =>   |- ((ph /\ ps /\ ch) -> th)
Theorem	biimp3ar 926	Infer implication from a logical equivalence. Similar to biimpar 417.
|- ((ph /\ ps) -> (ch <-> th))   =>   |- ((ph /\ ps /\ th) -> ch)
Theorem	3anandis 927	Inference that undistributes a triple conjunction in the antecedent.
|- (((ph /\ ps) /\ (ph /\ ch) /\ (ph /\ th)) -> ta)   =>   |- ((ph /\ (ps /\ ch /\ th)) -> ta)
Theorem	3anandirs 928	Inference that undistributes a triple conjunction in the antecedent.
|- (((ph /\ th) /\ (ps /\ th) /\ (ch /\ th)) -> ta)   =>   |- (((ph /\ ps /\ ch) /\ th) -> ta)
Theorem	ecase23d 929	Deduction for elimination by cases.
|- (ph -> -. ch)   &   |- (ph -> -. th)   &   |- (ph -> (ps \/ ch \/ th))   =>   |- (ph -> ps)
Theorem	3ecase 930	Inference for elimination by cases.
|- (-. ph -> th)   &   |- (-. ps -> th)   &   |- (-. ch -> th)   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- th
Other axiomatizations of classical propositional calculus
Derive the Lukasiewicz axioms from Meredith's sole axiom
Theorem	meredith 931	Carew Meredith's sole axiom for propositional calculus. This amazing formula is thought to be the shortest possible single axiom for propositional calculus with inference rule ax-mp 7, where negation and implication are primitive. Here we prove Meredith's axiom from ax-1 4, ax-2 5, and ax-3 6. Then from it we derive the Lukasiewicz axioms luk-1 945, luk-2 946, and luk-3 947. Using these we finally re-derive our axioms as ax1 956, ax2 957, and ax3 958, thus proving the equivalence of all three systems. C. A. Meredith, "Single Axioms for the Systems (C,N), (C,O) and (A,N) of the Two-Valued Propositional Calculus," The Journal of Computing Systems vol. 1 (1953), pp. 155-164. Meredith claimed to be close to a proof that this axiom is the shortest possible, but the proof was apparently never completed. An obscure Irish lecturer, Meredith (1904-1976) became enamored with logic somewhat late in life after attending talks by Lukasiewicz and produced many remarkable results such as this axiom. From his obituary: "He did logic whenever time and opportunity presented themselves, and he did it on whatever materials came to hand: in a pub, his favored pint of porter within reach, he would use the inside of cigarette packs to write proofs for logical colleagues."
|- (((((ph -> ps) -> (-. ch -> -. th)) -> ch) -> ta) -> ((ta -> ph) -> (th -> ph)))
Theorem	merlem1 932	Step 3 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (The step numbers refer to Meredith's original paper.)
|- (((ch -> (-. ph -> ps)) -> ta) -> (ph -> ta))
Theorem	merlem2 933	Step 4 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (((ph -> ph) -> ch) -> (th -> ch))
Theorem	merlem3 934	Step 7 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (((ps -> ch) -> ph) -> (ch -> ph))
Theorem	merlem4 935	Step 8 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (ta -> ((ta -> ph) -> (th -> ph)))
Theorem	merlem5 936	Step 11 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- ((ph -> ps) -> (-. -. ph -> ps))
Theorem	merlem6 937	Step 12 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (ch -> (((ps -> ch) -> ph) -> (th -> ph)))
Theorem	merlem7 938	Between steps 14 and 15 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (ph -> (((ps -> ch) -> th) -> (((ch -> ta) -> (-. th -> -. ps)) -> th)))
Theorem	merlem8 939	Step 15 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (((ps -> ch) -> th) -> (((ch -> ta) -> (-. th -> -. ps)) -> th))
Theorem	merlem9 940	Step 18 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (((ph -> ps) -> (ch -> (th -> (ps -> ta)))) -> (et -> (ch -> (th -> (ps -> ta)))))
Theorem	merlem10 941	Step 19 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- ((ph -> (ph -> ps)) -> (th -> (ph -> ps)))
Theorem	merlem11 942	Step 20 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- ((ph -> (ph -> ps)) -> (ph -> ps))
Theorem	merlem12 943	Step 28 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (((th -> (-. -. ch -> ch)) -> ph) -> ph)
Theorem	merlem13 944	Step 35 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- ((ph -> ps) -> (((th -> (-. -. ch -> ch)) -> -. -. ph) -> ps))
Theorem	luk-1 945	1 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom.
|- ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))
Theorem	luk-2 946	2 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom.
|- ((-. ph -> ph) -> ph)
Theorem	luk-3 947	3 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom.
|- (ph -> (-. ph -> ps))
Derive the standard axioms from the Lukasiewicz axioms
Theorem	luklem1 948	Used to rederive standard propositional axioms from Lukasiewicz'.
|- (ph -> ps)   &   |- (ps -> ch)   =>   |- (ph -> ch)
Theorem	luklem2 949	Used to rederive standard propositional axioms from Lukasiewicz'.
|- ((ph -> -. ps) -> (((ph -> ch) -> th) -> (ps -> th)))
Theorem	luklem3 950	Used to rederive standard propositional axioms from Lukasiewicz'.
|- (ph -> (((-. ph -> ps) -> ch) -> (th -> ch)))
Theorem	luklem4 951	Used to rederive standard propositional axioms from Lukasiewicz'.
|- ((((-. ph -> ph) -> ph) -> ps) -> ps)
Theorem	luklem5 952	Used to rederive standard propositional axioms from Lukasiewicz'.
|- (ph -> (ps -> ph))
Theorem	luklem6 953	Used to rederive standard propositional axioms from Lukasiewicz'.
|- ((ph -> (ph -> ps)) -> (ph -> ps))
Theorem	luklem7 954	Used to rederive standard propositional axioms from Lukasiewicz'.
|- ((ph -> (ps -> ch)) -> (ps -> (ph -> ch)))
Theorem	luklem8 955	Used to rederive standard propositional axioms from Lukasiewicz'.
|- ((ph -> ps) -> ((ch -> ph) -> (ch -> ps)))
Theorem	ax1 956	Standard propositional axiom derived from Lukasiewicz axioms.
|- (ph -> (ps -> ph))
Theorem	ax2 957	Standard propositional axiom derived from Lukasiewicz axioms.
|- ((ph -> (ps -> ch)) -> ((ph -> ps) -> (ph -> ch)))
Theorem	ax3 958	Standard propositional axiom derived from Lukasiewicz axioms.
|- ((-. ph -> -. ps) -> (ps -> ph))
Logical 'nand' (Sheffer stroke)
Syntax	wnand 959	Extend wff definition to include 'nand'.
wff (ph -/\ ps)
Definition	df-nand 960	Define incompatibility ('not-and' or 'nand'). This is also called the Sheffer stroke, represented by a vertical bar, but we use a different symbol to avoid ambiguity with other uses of the vertical bar.
|- ((ph -/\ ps) <-> -. (ph /\ ps))
Derive Nicod's axiom from the standard axioms
Theorem	nic-justlem 961	Lemma for handling nested 'nand's.
Theorem	nic-justim 962	Show equivalence between implication and the Nicod version. To derive nic-dfim 965, apply nic-justbi 964.
|- ((ph -> ps) <-> (ph -/\ (ps -/\ ps)))
Theorem	nic-justneg 963	Show equivalence between negation and the Nicod version. To derive nic-dfneg 966, apply nic-justbi 964.
|- (-. ps <-> (ps -/\ ps))
Theorem	nic-justbi 964	Show equivalence between the bidirectional and the Nicod version. (Contributed by Jeff Hoffman, 19-Nov-2007.)
|- ((ph <-> ps) <-> ((ph -/\ ps) -/\ ((ph -/\ ph) -/\ (ps -/\ ps))))
Theorem	nic-dfim 965	Define implication in terms of 'nand'. Analogous to ((ph -/\ (ps -/\ ps)) <-> (ph -> ps)). In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to a definition ($a statement).
|- (((ph -/\ (ps -/\ ps)) -/\ (ph -> ps)) -/\ (((ph -/\ (ps -/\ ps)) -/\ (ph -/\ (ps -/\ ps))) -/\ ((ph -> ps) -/\ (ph -> ps))))
Theorem	nic-dfneg 966	Define negation in terms of 'nand'. Analogous to ((ph -/\ ph) <-> -. ph). In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to a definition ($a statement).
|- (((ph -/\ ph) -/\ -. ph) -/\ (((ph -/\ ph) -/\ (ph -/\ ph)) -/\ (-. ph -/\ -. ph)))
Theorem	nic-mp 967	Derive Nicod's rule of modus ponens using 'nand', from the standard one. Although the major and minor premise together also imply ch, this form is necessary for useful derivations from nic-ax 969. In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to an axiom ($a statement). (Contributed by Jeff Hoffman, 19-Nov-2007.)
|- ph   &   |- (ph -/\ (ch -/\ ps))   =>   |- ps
Theorem	nic-mpALT 968	A direct proof of nic-mp 967.
|- ph   &   |- (ph -/\ (ch -/\ ps))   =>   |- ps
Theorem	nic-ax 969	Nicod's axiom derived from the standard ones. See _Intro. to Math. Phil._ by B. Russell, p. 152. Like meredith 931, the usual axioms can be derived from this and vice versa. Unlike meredith 931, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g. { nic-ax 969, nic-mp 967 } is equivalent to { luk-1 945, luk-2 946, luk-3 947, ax-mp 7 }. In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to an axiom ($a statement). (Contributed by Jeff Hoffman, 19-Nov-2007.)
|- ((ph -/\ (ch -/\ ps)) -/\ ((ta -/\ (ta -/\ ta)) -/\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th)))))
Theorem	nic-axALT 970	A direct proof of nic-ax 969.
|- ((ph -/\ (ch -/\ ps)) -/\ ((ta -/\ (ta -/\ ta)) -/\ ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th)))))
Derive the Lukasiewicz axioms from Nicod's axiom
Theorem	nic-imp 971	Inference for nic-mp 967 using nic-ax 969 as major premise. (Contributed by Jeff Hoffman, 17-Nov-2007.)
|- (ph -/\ (ch -/\ ps))   =>   |- ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th)))
Theorem	nic-idlem1 972	Lemma for nic-id 974.
Theorem	nic-idlem2 973	Lemma for nic-id 974. Inference used by nic-id 974.
Theorem	nic-id 974	Theorem id 59 expressed with -/\. (Contributed by Jeff Hoffman, 17-Nov-2007.)
|- (ta -/\ (ta -/\ ta))
Theorem	nic-swap 975	-/\ is symmetric. (Contributed by Jeff Hoffman, 17-Nov-2007.)
|- ((th -/\ ph) -/\ ((ph -/\ th) -/\ (ph -/\ th)))
Theorem	nic-isw1 976	Inference version of nic-swap 975. (Contributed by Jeff Hoffman, 17-Nov-2007.)
|- (th -/\ ph)   =>   |- (ph -/\ th)
Theorem	nic-isw2 977	Inference for swapping nested terms. (Contributed by Jeff Hoffman, 17-Nov-2007.)
|- (ps -/\ (th -/\ ph))   =>   |- (ps -/\ (ph -/\ th))
Theorem	nic-iimp1 978	Inference version of nic-imp 971 using right-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.)
|- (ph -/\ (ch -/\ ps))   &   |- (th -/\ ch)   =>   |- (th -/\ ph)
Theorem	nic-iimp2 979	Inference version of nic-imp 971 using left-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.)
|- ((ph -/\ ps) -/\ (ch -/\ ch))   &   |- (th -/\ ph)   =>   |- (th -/\ (ch -/\ ch))
Theorem	nic-idel 980	Inference to remove the trailing term. (Contributed by Jeff Hoffman, 17-Nov-2007.)
|- (ph -/\ (ch -/\ ps))   =>   |- (ph -/\ (ch -/\ ch))
Theorem	nic-ich 981	Chained inference. (Contributed by Jeff Hoffman, 17-Nov-2007.)
|- (ph -/\ (ps -/\ ps))   &   |- (ps -/\ (ch -/\ ch))   =>   |- (ph -/\ (ch -/\ ch))
Theorem	nic-idbl 982	Double the terms. Since doubling is the same as negation, this can be viewed as a contraposition Inference. (Contributed by Jeff Hoffman, 17-Nov-2007.)
|- (ph -/\ (ps -/\ ps))   =>   |- ((ps -/\ ps) -/\ ((ph -/\ ph) -/\ (ph -/\ ph)))
Theorem	nic-bijust 983	For nic-* definitions, the biconditional connective is not used. Instead, definitions are made based on this form. nic-bi1 984 and nic-bi2 985 are used to convert the definitions into usable theorems about one side of the implication. (Contributed by Jeff Hoffman, 18-Nov-2007.)
|- ((ta -/\ ta) -/\ ((ta -/\ ta) -/\ (ta -/\ ta)))
Theorem	nic-bi1 984	Inference to extract one side of an implication from a definition
|- ((ph -/\ ps) -/\ ((ph -/\ ph) -/\ (ps -/\ ps)))   =>   |- (ph -/\ (ps -/\ ps))
Theorem	nic-bi2 985	Inference to extract the other side of an implication from a 'biconditional' definition.
|- ((ph -/\ ps) -/\ ((ph -/\ ph) -/\ (ps -/\ ps)))   =>   |- (ps -/\ (ph -/\ ph))
Theorem	nic-stdmp 986	Derive the standard modus ponens from nic-mp 967. (Contributed by Jeff Hoffman, 18-Nov-2007.)
|- ph   &   |- (ph -> ps)   =>   |- ps
Theorem	nic-luk1 987	Proof of luk-1 945 from nic-ax 969 and nic-mp 967 (and definitions nic-dfim 965 and nic-dfneg 966). Note that the standard axioms ax-1 4, ax-2 5, and ax-3 6 are proved from the Lukasiewicz axioms by theorems ax1 956, ax2 957, and ax3 958. (Contributed by Jeff Hoffman, 18-Nov-2007.)
|- ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))
Theorem	nic-luk2 988	Proof of luk-2 946 from nic-ax 969 and nic-mp 967. (Contributed by Jeff Hoffman, 18-Nov-2007.)
|- ((-. ph -> ph) -> ph)
Theorem	nic-luk3 989	Proof of luk-3 947 from nic-ax 969 and nic-mp 967. (Contributed by Jeff Hoffman, 18-Nov-2007.)
|- (ph -> (-. ph -> ps))
Predicate calculus axiomatization
The axioms of predicate calculus
Syntax	wal 990	Extend wff definition to include the universal quantifier ('for all'). A.xph is read "ph (phi) is true for all x." Typically, in its final application ph would be replaced with a wff containing a (free) occurrence of the variable x, for example x = y. In a universe with a finite number of objects, "for all" is equivalent to a big conjunction (AND) with one wff for each possible case of x. When the universe is infinite (as with set theory), such a propositional-calculus equivalent is not possible because an infinitely long formula has no meaning, but conceptually the idea is the same.
wff A.xph
Syntax	cv 991	This syntax construction states that a variable x, which has been declared to be a set variable by $f statement vx, is also a class expression. This can be justified informally as follows. We know that the class builder {y | y e. x} is a class by cab 1505. Since (when y is distinct from x) we have x = {y | y e. x} by cvjust 1513, we can argue that that the syntax "class x" can be viewed as an abbreviation for "class {y | y e. x}". See the discussion under the definition of class in [Jech] p. 4 showing that "Every set can be considered to be a class." While it is tempting and perhaps occasionally useful to view cv 991 as a "type conversion" from a set variable to a class variable, keep in mind that cv 991 is intrinsically no different from any other class-building syntax such as cab 1505, cun 2097, or c0 2332. (The description above applies to set theory, not predicate calculus. The purpose of introducing class x here, and not in set theory where it belongs, is to allow us to express i.e. "prove" the weq 993 of predicate calculus from the wceq 992 of set theory, so that we don't "overload" the = connective with two syntax definitions. This is done to prevent ambiguity that would complicate some Metamath parsers.)
class x
Syntax	wceq 992	Extend wff definition to include class equality. (The purpose of introducing wff A = B here, and not in set theory where it belongs, is to allow us to express i.e. "prove" the weq 993 of predicate calculus in terms of the wceq 992 of set theory, so that we don't "overload" the = connective with two syntax definitions. This is done to prevent ambiguity that would complicate some Metamath parsers. For example, some parsers - although not the Metamath program - stumble on the fact that the = in x = y could be the = of either weq 993 or wceq 992, although mathematically it makes no difference. The class variables A and B are introduced temporarily for the purpose of this definition but otherwise not used in predicate calculus. See df-cleq 1511 for more information on the set theory usage of wceq 992.)
wff A = B
Theorem	weq 993	Extend wff definition to include atomic formulas using the equality predicate. (Instead of introducing weq 993 as an axiomatic statement, as was done in an older version of this database, we introduce it by "proving" a special case of set theory's more general wceq 992. This lets us avoid overloading the = connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq 993 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 992. Note: To see the proof steps of this syntax proof, type "show proof weq /all" in the Metamath program.)
wff x = y
Syntax	wcel 994	Extend wff definition to include the membership connective between classes. (The purpose of introducing wff A e. B here is to allow us to express i.e. "prove" the wel 995 of predicate calculus in terms of the wceq 992 of set theory, so that we don't "overload" the e. connective with two syntax definitions. This is done to prevent ambiguity that would complicate some Metamath parsers. The class variables A and B are introduced temporarily for the purpose of this definition but otherwise not used in predicate calculus. See df-clab 1506 for more information on the set theory usage of wcel 994.)
wff A e. B
Theorem	wel 995	Extend wff definition to include atomic formulas with the epsilon (membership) predicate. This is read "x is an element of y," "x is a member of y," "x belongs to y," or "y contains x." Note: The phrase "y includes x" means "x is a subset of y;" to use it also for x e. y, as some authors occasionally do, is poor form and causes confusion, according to George Boolos (1992 lecture at MIT). This syntactical construction introduces a binary non-logical predicate symbol e. (epsilon) into our predicate calculus. We will eventually use it for the membership predicate of set theory, but that is irrelevant at this point: the predicate calculus axioms for e. apply to any arbitrary binary predicate symbol. "Non-logical" means that the predicate is presumed to have additional properties beyond the realm of predicate calculus, although these additional properties are not specified by predicate calculus itself but rather by the axioms of a theory (in our case set theory) added to predicate calculus. "Binary" means that the predicate has two arguments. (Instead of introducing wel 995 as an axiomatic statement, as was done in an older version of this database, we introduce it by "proving" a special case of set theory's more general wcel 994. This lets us avoid overloading the e. connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 995 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 994. Note: To see the proof steps of this syntax proof, type "show proof wel /all" in the Metamath program.)
wff x e. y
Axiom	ax-5 996	Axiom of Quantified Implication. Axiom C4 of [Monk2] p. 105.
|- (A.x(ph -> ps) -> (A.xph -> A.xps))
Axiom	ax-6 997	Axiom of Quantified Negation. Axiom C5-2 of [Monk2] p. 113.
|- (-. A.xph -> A.x -. A.xph)
Axiom	ax-7 998	Axiom of Quantifier Commutation. This axiom says universal quantifiers can be swapped. One of the 4 axioms of pure predicate calculus. Axiom scheme C6' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Lemma 12 of [Monk2] p. 109 and Axiom C5-3 of [Monk2] p. 113. An alternate axiomatization could use ax467 1059 in place of ax-4 1009, ax-6o 1014, and ax-7 998.
|- (A.xA.yph -> A.yA.xph)
Axiom	ax-gen 999	Rule of Generalization. The postulated inference rule of pure predicate calculus. See e.g. Rule 2 of [Hamilton] p. 74. This rule says that if something is unconditionally true, then it is true for all values of a variable. For example, if we have proved x = x, we can conclude A.xx = x or even A.yx = x. Theorem a4i 1018 shows we can go the other way also: in other words we can add or remove universal quantifiers from the beginning of any theorem as required.
|- ph   =>   |- A.xph
Axiom	ax-8 1000	Axiom of Equality. One of the equality and substitution axioms of predicate calculus with equality. This is similar to, but not quite, a transitive law for equality (proved later as equtr 1168). Axiom scheme C8' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Axiom C7 of [Monk2] p. 105. Axioms ax-8 1000 through ax-16 1247 are the axioms having to do with equality, substitution, and logical properties of our binary predicate e. (which later in set theory will mean "is a member of"). Note that all axioms except ax-16 1247 and ax-17 1007 are still valid even when x, y, and z are replaced with the same variable because they do not have any distinct variable (Metamath's $d) restrictions. Distinct variable restrictions are required for ax-16 1247 and ax-17 1007 only.
|- (x = y -> (x = z -> y = z))