Metamath Proof Explorer - mmtheorems13

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 - 1201-1300 - Page 13 of 58

Type	Label	Description
Statement
Syntax	wral 1201	Extend wff notation to include restricted universal quantification.
wff A.x e. A ph
Syntax	wrex 1202	Extend wff notation to include restricted existential quantification.
wff E.x e. A ph
Syntax	wreu 1203	Extend wff notation to include restricted existential uniqueness.
wff E!x e. A ph
Syntax	crab 1204	Extend class notation to include restricted class abstractions.
class {x e. A | ph}
Definition	df-ral 1205	Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22.
|- (A.x e. A ph <-> A.x(x e. A -> ph))
Definition	df-rex 1206	Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22.
|- (E.x e. A ph <-> E.x(x e. A /\ ph))
Definition	df-reu 1207	Define restricted existential uniqueness.
|- (E!x e. A ph <-> E!x(x e. A /\ ph))
Definition	df-rab 1208	Define a restricted class abstraction, which is the class of all x in A such that ph is true. Definition of [TakeutiZaring] p. 20.
|- {x e. A | ph} = {x | (x e. A /\ ph)}
Theorem	ralnex 1209	Relationship between restricted universal and existential quantifiers.
|- (A.x e. A -. ph <-> -. E.x e. A ph)
Theorem	rexnal 1210	Relationship between restricted universal and existential quantifiers.
|- (E.x e. A -. ph <-> -. A.x e. A ph)
Theorem	dfral2 1211	Relationship between restricted universal and existential quantifiers.
|- (A.x e. A ph <-> -. E.x e. A -. ph)
Theorem	dfrex2 1212	Relationship between restricted universal and existential quantifiers.
|- (E.x e. A ph <-> -. A.x e. A -. ph)
Theorem	biralda 1213	Formula-building rule for restricted universal quantifier (deduction rule).
|- (ph -> A.xph)   &   |- ((ph /\ x e. A) -> (ps <-> ch))   =>   |- (ph -> (A.x e. A ps <-> A.x e. A ch))
Theorem	birexda 1214	Formula-building rule for restricted existential quantifier (deduction rule).
|- (ph -> A.xph)   &   |- ((ph /\ x e. A) -> (ps <-> ch))   =>   |- (ph -> (E.x e. A ps <-> E.x e. A ch))
Theorem	biraldva 1215	Formula-building rule for restricted universal quantifier (deduction rule).
|- ((ph /\ x e. A) -> (ps <-> ch))   =>   |- (ph -> (A.x e. A ps <-> A.x e. A ch))
Theorem	birexdva 1216	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	birald 1217	Formula-building rule for restricted universal quantifier (deduction rule).
|- (ph -> A.xph)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> (A.x e. A ps <-> A.x e. A ch))
Theorem	birexd 1218	Formula-building rule for restricted existential quantifier (deduction rule).
|- (ph -> A.xph)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> (E.x e. A ps <-> E.x e. A ch))
Theorem	biraldv 1219	Formula-building rule for restricted universal quantifier (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (A.x e. A ps <-> A.x e. A ch))
Theorem	birexdv 1220	Formula-building rule for restricted existential quantifier (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> (E.x e. A ps <-> E.x e. A ch))
Theorem	biraldv2 1221	Formula-building rule for restricted universal quantifier (deduction rule).
|- (ph -> ((x e. A -> ps) <-> (x e. B -> ch)))   =>   |- (ph -> (A.x e. A ps <-> A.x e. B ch))
Theorem	birexdv2 1222	Formula-building rule for restricted existential quantifier (deduction rule).
|- (ph -> ((x e. A /\ ps) <-> (x e. B /\ ch)))   =>   |- (ph -> (E.x e. A ps <-> E.x e. B ch))
Theorem	biral 1223	Inference adding restricted universal quantifier to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (A.x e. A ph <-> A.x e. A ps)
Theorem	birex 1224	Inference adding restricted existential quantifier to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (E.x e. A ph <-> E.x e. A ps)
Theorem	bi2ral 1225	Inference adding 2 restricted universal quantifiers to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (A.x e. A A.y e. B ph <-> A.x e. A A.y e. B ps)
Theorem	bi2rex 1226	Inference adding 2 restricted existential quantifiers to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (E.x e. A E.y e. B ph <-> E.x e. A E.y e. B ps)
Theorem	birex2 1227	Inference adding different restricted existential quantifiers to each side of an equivalence.
|- ((x e. A /\ ph) <-> (x e. B /\ ps))   =>   |- (E.x e. A ph <-> E.x e. B ps)
Theorem	birala 1228	Inference adding restricted universal quantifier to both sides of an equivalence.
|- (x e. A -> (ph <-> ps))   =>   |- (A.x e. A ph <-> A.x e. A ps)
Theorem	birexa 1229	Inference adding restricted existential quantifier to both sides of an equivalence.
|- (x e. A -> (ph <-> ps))   =>   |- (E.x e. A ph <-> E.x e. A ps)
Theorem	bi2rexa 1230	Inference adding 2 restricted existential quantifiers to both sides of an equivalence.
|- ((x e. A /\ y e. B) -> (ph <-> ps))   =>   |- (E.x e. A E.y e. B ph <-> E.x e. A E.y e. B ps)
Theorem	r2al 1231	Double restricted universal quantification.
|- (A.x e. A A.y e. B ph <-> A.xA.y((x e. A /\ y e. B) -> ph))
Theorem	bi2ralda 1232	Formula-building rule for restricted universal quantifier (deduction rule).
|- (ph -> A.xph)   &   |- (ph -> A.yph)   &   |- ((ph /\ (x e. A /\ y e. B)) -> (ps <-> ch))   =>   |- (ph -> (A.x e. A A.y e. B ps <-> A.x e. A A.y e. B ch))
Theorem	bi2raldva 1233	Formula-building rule for restricted universal quantifier (deduction rule).
|- ((ph /\ (x e. A /\ y e. B)) -> (ps <-> ch))   =>   |- (ph -> (A.x e. A A.y e. B ps <-> A.x e. A A.y e. B ch))
Theorem	bi2rexdva 1234	Formula-building rule for restricted existential quantifier (deduction rule).
|- ((ph /\ (x e. A /\ y e. B)) -> (ps <-> ch))   =>   |- (ph -> (E.x e. A E.y e. B ps <-> E.x e. A E.y e. B ch))
Theorem	risset 1235	Two ways to say "A belongs to B".
|- (A e. B <-> E.x e. B x = A)
Theorem	hbral 1236	Bound-variable hypothesis builder for restricted quantification.
|- (y e. A -> A.x y e. A)   &   |- (ph -> A.xph)   =>   |- (A.y e. A ph -> A.xA.y e. A ph)
Theorem	hbra1 1237	x is not free in A.x e. Aph.
|- (A.x e. A ph -> A.xA.x e. A ph)
Theorem	hbrex 1238	Bound-variable hypothesis builder for restricted quantification.
|- (y e. A -> A.x y e. A)   &   |- (ph -> A.xph)   =>   |- (E.y e. A ph -> A.xE.y e. A ph)
Theorem	hbre1 1239	x is not free in E.x e. Aph.
|- (E.x e. A ph -> A.xE.x e. A ph)
Theorem	r3al 1240	Triple restricted universal quantification.
|- (A.x e. A A.y e. B A.z e. C ph <-> A.xA.yA.z((x e. A /\ y e. B /\ z e. C) -> ph))
Theorem	r2ex 1241	Double restricted existential quantification.
|- (E.x e. A E.y e. B ph <-> E.xE.y((x e. A /\ y e. B) /\ ph))
Theorem	rexex 1242	Restricted existence implies existence.
|- (E.x e. A ph -> E.xph)
Theorem	ra4 1243	Restricted specialization.
|- (A.x e. A ph -> (x e. A -> ph))
Theorem	ra4e 1244	Restricted specialization.
|- ((x e. A /\ ph) -> E.x e. A ph)
Theorem	ra42 1245	Restricted specialization.
|- (A.x e. A A.y e. B ph -> ((x e. A /\ y e. B) -> ph))
Theorem	rspec 1246	Specialization rule for restricted quantification.
|- A.x e. A ph   =>   |- (x e. A -> ph)
Theorem	rgen 1247	Generalization rule for restricted quantification.
|- (x e. A -> ph)   =>   |- A.x e. A ph
Theorem	rgen2 1248	Generalization rule for restricted quantification. Note that x and y needn't be distinct.
|- ((x e. A /\ y e. A) -> ph)   =>   |- A.x e. A A.y e. A ph
Theorem	mprg 1249	Modus ponens combined with restricted generalization.
|- (A.x e. A ph -> ps)   &   |- (x e. A -> ph)   =>   |- ps
Theorem	mprgbir 1250	Modus ponens on biconditional combined with restricted generalization.
|- (ph <-> A.x e. A ps)   &   |- (x e. A -> ps)   =>   |- ph
Theorem	r19.20 1251	Distribution of restricted quantification over implication.
|- (A.x e. A (ph -> ps) -> (A.x e. A ph -> A.x e. A ps))
Theorem	r19.20i2 1252	Inference quantifying both antecedent and consequent.
|- ((x e. A -> ph) -> (x e. B -> ps))   =>   |- (A.x e. A ph -> A.x e. B ps)
Theorem	r19.20i 1253	Inference quantifying both antecedent and consequent.
|- (x e. A -> (ph -> ps))   =>   |- (A.x e. A ph -> A.x e. A ps)
Theorem	r19.20si 1254	Inference quantifying both antecedent and consequent, with strong hypothesis.
|- (ph -> ps)   =>   |- (A.x e. A ph -> A.x e. A ps)
Theorem	r19.20da 1255	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90.
|- (ph -> A.xph)   &   |- ((ph /\ x e. A) -> (ps -> ch))   =>   |- (ph -> (A.x e. A ps -> A.x e. A ch))
Theorem	r19.20dva 1256	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90.
|- ((ph /\ x e. A) -> (ps -> ch))   =>   |- (ph -> (A.x e. A ps -> A.x e. A ch))
Theorem	r19.20sdv 1257	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- (ph -> (A.x e. A ps -> A.x e. A ch))
Theorem	r19.21ai 1258	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
|- (ph -> A.xph)   &   |- (ph -> (x e. A -> ps))   =>   |- (ph -> A.x e. A ps)
Theorem	r19.21aiv 1259	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
|- (ph -> (x e. A -> ps))   =>   |- (ph -> A.x e. A ps)
Theorem	r19.21v 1260	Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers.
|- (A.x e. A (ph -> ps) <-> (ph -> A.x e.