Metamath Proof Explorer - mmtheorems14

Jump to page: 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-5787

Statement List for Metamath Proof Explorer - 1301-1400 - Page 14 of 58

Type	Label	Description
Statement
Theorem	r19.40 1301	Restricted quantifier version of Theorem 19.40 of [Margaris] p. 90.
|- (E.x e. A (ph /\ ps) -> (E.x e. A ph /\ E.x e. A ps))
Theorem	r19.41v 1302	Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90.
|- (E.x e. A (ph /\ ps) <-> (E.x e. A ph /\ ps))
Theorem	r19.42v 1303	Restricted version of Theorem 19.42 of [Margaris] p. 90.
|- (E.x e. A (ph /\ ps) <-> (ph /\ E.x e. A ps))
Theorem	r19.43 1304	Restricted version of Theorem 19.43 of [Margaris] p. 90.
|- (E.x e. A (ph \/ ps) <-> (E.x e. A ph \/ E.x e. A ps))
Theorem	r19.44av 1305	One direction of a restricted quantifier version of Theorem 19.44 of [Margaris] p. 90. The other direction doesn't hold when A is empty.
|- (E.x e. A (ph \/ ps) -> (E.x e. A ph \/ ps))
Theorem	r19.45av 1306	Restricted version of one direction of Theorem 19.45 of [Margaris] p. 90. (The other direction doesn't hold when A is empty.)
|- (E.x e. A (ph \/ ps) -> (ph \/ E.x e. A ps))
Theorem	hbreu1 1307	x is not free in E!x e. Aph.
|- (E!x e. A ph -> A.xE!x e. A ph)
Theorem	rabid 1308	An "identity" law of concretion for restricted abstraction. Special case of Definition 2.1 of [Quine] p. 16.
|- (x e. {x e. A | ph} <-> (x e. A /\ ph))
Theorem	rabid2 1309	An "identity" law for restricted class abstraction.
|- (A = {x e. A | ph} <-> A.x e. A ph)
Theorem	hbrab1 1310	The abstraction variable in a restricted class abstraction isn't free.
|- (y e. {x e. A | ph} -> A.x y e. {x e. A | ph})
Theorem	hbrab 1311	A variable not free in a wff remains so in a restricted class abstraction.
|- (ph -> A.xph)   &   |- (z e. A -> A.x z e. A)   =>   |- (z e. {y e. A | ph} -> A.x z e. {y e. A | ph})
Theorem	ralcom 1312	Commutation of restricted quantifiers.
|- (A.x e. A A.y e. B ph <-> A.y e. B A.x e. A ph)
Theorem	rexcom 1313	Commutation of restricted quantifiers.
|- (E.x e. A E.y e. B ph <-> E.y e. B E.x e. A ph)
Theorem	ralcom2 1314	Commutation of restricted quantifiers. Note that x and y needn't be distinct (this makes the proof longer but illustrates the use of ddelim 1000).
|- (A.x e. A A.y e. A ph -> A.y e. A A.x e. A ph)
Theorem	ralcom3 1315	A commutative law for restricted quantifiers that swaps the domain of the restriction.
|- (A.x e. A (x e. B -> ph) <-> A.x e. B (x e. A -> ph))
Theorem	reeanv 1316	Rearrange existential quantifiers.
|- (E.x e. A E.y e. B (ph /\ ps) <-> (E.x e. A ph /\ E.y e. B ps))
Theorem	bireudva 1317	Formula-building rule for restricted existential quantifier (deduction rule).
|- ((ph /\ x e. A) -> (ps <-> ch))   =>   |- (ph -> (E!x e. A ps <-> E!x e. A ch))
Theorem	bireudv 1318	Formula-building rule for restricted existential quantifier (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (E!x e. A ps <-> E!x e. A ch))
Theorem	bireua 1319	Formula-building rule for restricted existential quantifier (inference rule).
|- (x e. A -> (ph <-> ps))   =>   |- (E!x e. A ph <-> E!x e. A ps)
Theorem	bireu 1320	Formula-building rule for restricted existential quantifier (inference rule).
|- (ph <-> ps)   =>   |- (E!x e. A ph <-> E!x e. A ps)
Theorem	raleqf 1321	Equality theorem for restricted universal quantifier, with bound variable hypotheses instead of distinct variable restrictions.
|- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   =>   |- (A = B -> (A.x e. A ph <-> A.x e. B ph))
Theorem	rexeqf 1322	Equality theorem for restricted existential quantifier, with bound variable hypotheses instead of distinct variable restrictions.
|- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   =>   |- (A = B -> (E.x e. A ph <-> E.x e. B ph))
Theorem	reueqf 1323	Equality theorem for restricted uniqueness quantifier, with bound variable hypotheses instead of distinct variable restrictions.
|- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   =>   |- (A = B -> (E!x e. A ph <-> E!x e. B ph))
Theorem	raleq 1324	Equality theorem for restricted universal quantifier.
|- (A = B -> (A.x e. A ph <-> A.x e. B ph))
Theorem	rexeq 1325	Equality theorem for restricted existential quantifier.
|- (A = B -> (E.x e. A ph <-> E.x e. B ph))
Theorem	reueq 1326	Equality theorem for restricted uniqueness quantifier.
|- (A = B -> (E!x e. A ph <-> E!x e. B ph))
Theorem	raleqd 1327	Equality deduction for restricted universal quantifier.
|- (A = B -> (ph <-> ps))   =>   |- (A = B -> (A.x e. A ph <-> A.x e. B ps))
Theorem	rexeqd 1328	Equality deduction for restricted existential quantifier.
|- (A = B -> (ph <-> ps))   =>   |- (A = B -> (E.x e. A ph <-> E.x e. B ps))
Theorem	reueqd 1329	Equality deduction for restricted uniqueness quantifier.
|- (A = B -> (ph <-> ps))   =>   |- (A = B -> (E!x e. A ph <-> E!x e. B ps))
Theorem	cbvralf 1330	Rule used to change bound variables with implicit substitution.
|- (z e. A -> A.x z e. A)   &   |- (z e. A -> A.y z e. A)   &   |- (ph -> A.yph)   &   |- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- (A.x e. A ph <-> A.y e. A ps)
Theorem	cbvral 1331	Rule used to change bound variables with implicit substitution.
|- (ph -> A.yph)   &   |- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- (A.x e. A ph <-> A.y e. A ps)
Theorem	cbvrex 1332	Rule used to change bound variables with implicit substitution.
|- (ph -> A.yph)   &   |- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- (E.x e. A ph <-> E.y e. A ps)
Theorem	cbvralv 1333	Change the bound variable of a restricted universal quantifier using implicit substitution.
|- (x = y -> (ph <-> ps))   =>   |- (A.x e. A ph <-> A.y e. A ps)
Theorem	cbvrexv 1334	Change the bound variable of a restricted existential quantifier using implicit substitution.
|- (x = y -> (ph <-> ps))   =>   |- (E.x e. A ph <-> E.y e. A ps)
Theorem	cbvreuv 1335	Change the bound variable of a restricted uniqueness quantifier using implicit substitution.
|- (x = y -> (ph <-> ps))   =>   |- (E!x e. A ph <-> E!y e. A ps)
Theorem	cbvral2v 1336	Change bound variables of double restricted universal quantification, using implicit substitution.
|- (x = z -> (ph <-> ch))   &   |- (y = w -> (ch <-> ps))   =>   |- (A.x e. A A.y e. B ph <-> A.z e. A A.w e. B ps)
Theorem	reurex 1337	Restricted unique existence implies restricted existence.
|- (E!x e. A ph -> E.x e. A ph)
Theorem	reu2 1338	A way of expressing restricted uniqueness.
|- (E!x e. A ph <-> (E.x e. A ph /\ A.x e. A A.y e. A ((ph /\ [y / x]ph) -> x = y)))
Theorem	reu5 1339	Restricted uniqueness in terms of "at most one".
|- (E!x e. A ph <-> (E.x e. A ph /\ E*x(x e. A /\ ph)))
Theorem	reu4 1340	Restricted uniqueness using implicit substitution.
|- (x = y -> (ph <-> ps))   =>   |- (E!x e. A ph <-> (E.x e. A ph /\ A.x e. A A.y e. A ((ph /\ ps) -> x = y)))
Theorem	2reuswap 1341	A condition allowing swap of uniqueness and existential quantifiers.
|- (A.x e. A E*y(y e. A /\ ph) -> (E!x e. A E.y e. A ph -> E!y e. A E.x e. A ph))
Theorem	birabi 1342	Equivalent wff's yield equal restricted class abstractions (inference rule).
|- (x e. A -> (ps <-> ch))   =>   |- {x e. A | ps} = {x e. A | ch}
Theorem	birabdv 1343	Equivalent wff's yield equal restricted class abstractions (deduction rule).
|- (ph -> (x e. A -> (ps <-> ch)))   =>   |- (ph -> {x e. A | ps} = {x e. A | ch})
Theorem	birabsdv 1344	Equivalent wff's yield equal restricted class abstractions (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> {x e. A | ps} = {x e. A | ch})
Theorem	rabeqf 1345	Equality theorem for restricted class abstractions, with bound variable hypotheses instead of distinct variable restrictions.
|- (y e. A -> A.x y e. A)   &   |- (y e. B -> A.x y e. B)   =>   |- (A = B -> {x e. A | ph} = {x e. B | ph})
Theorem	rabeq 1346	Equality theorem for restricted class abstractions.
|- (A = B -> {x e. A | ph} = {x e. B | ph})
Theorem	cleqrabi 1347	Inference rule from equality of a class variable and a restricted class abstraction.
|- A = {x e. B | ph}   =>   |- (x e. A <-> (x e. B /\ ph))
Syntax	cvv 1348	Extend class notation to include the universal class symbol.
class V
Definition	df-v 1349	Define the universal class. Definition 5.20 of [TakeutiZaring] p. 21.
|- V = {x | x = x}
Theorem	visset 1350	All set variables are sets (see isset 1351). Theorem 6.8 of [Quine] p. 43.
|- x e. V
Theorem	isset 1351	Two ways to say "A is a set": A class A is a member of the universal class V (see df-v 1349) if and only if the class A exists (i.e. there exists some set x equal to class A). Theorem 6.9 of [Quine] p. 43. Notational convention: We will use the notational device "A e. V" to mean "A is a set" very frequently, for example in uniex 1947. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 1948, in order to shorten certain proofs we use the antecedent A e. B instead of A e. V to mean "A is a set".
|- (A e. V <-> E.x x = A)
Theorem	isseti 1352	A way to say "A is a set" (inference rule).
|- A e. V   =>   |- E.x x = A
Theorem	issetri 1353	A way to say "A is a set" (inference rule).
|- E.x x = A   =>   |- A e. V
Theorem	elisset 1354	If a class is a member of another class, it is a set. Theorem 6.12 of [Quine] p. 44.
|- (A e. B -> A e. V)
Theorem	elisseti 1355	If a class is a member of another class, it is a set.
|- A e. B   =>   |- A e. V
Theorem	elex 1356	An element of a class exists.
|- (A e. B -> E.x x = A)
Theorem	ralv 1357	A universal quantifier restricted to the universe is unrestricted.
|- (A.x e. V ph <-> A.xph)
Theorem	rexv 1358	An existential quantifier restricted to the universe is unrestricted.
|- (E.x e. V ph <-> E.xph)
Theorem	rabab 1359	A class abstraction restricted to the universe is unrestricted.
|- {x e. V | ph} = {x | ph}
Theorem	ralcom4 1360	Commutation of restricted and unrestricted universal quantifiers.
|- (A.x e. A A.yph <-> A.yA.x e. A ph)
Theorem	rexcom4 1361	Commutation of restricted and unrestricted existential quantifiers.
|- (E.x e.