mmtheorems114 - 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-12230

Statement List for Metamath Proof Explorer - 11301-11400 - Page 114 of 123

Type	Label	Description
Statement
Theorem	issubcata 11301	The predicate "is a subcategory of" T.
⊢ D = (dom ‘T)    &   ⊢ C = (cod ‘T)    &   ⊢ R = (o ‘T)    &   ⊢ J = (id ‘T)    ⇒   ⊢ (T ∈ Cat → (U ∈ (SubCat ‘T) ↔ (U ∈ Cat ⋀ ((id ‘U) ⊆ J ⋀ ((dom ‘U) ⊆ D ⋀ (cod ‘U) ⊆ C) ⋀ (o ‘U) ⊆ R))))
Theorem	issubcatb 11302	The predicate "is a subcategory of" T.
⊢ D = (dom ‘T)    &   ⊢ C = (cod ‘T)    &   ⊢ R = (o ‘T)    &   ⊢ J = (id ‘T)    ⇒   ⊢ ((T ∈ Cat ⋀ U ∈ Cat) → (U ∈ (SubCat ‘T) ↔ ((id ‘U) ⊆ J ⋀ ((dom ‘U) ⊆ D ⋀ (cod ‘U) ⊆ C) ⋀ (o ‘U) ⊆ R)))
Theorem	besubbeca 11303	Lemma to simplify some subcategories related theorems .
⊢ (U ∈ (SubCat ‘T) → T ∈ Cat)
Theorem	catsbc 11304	A category belongs to the set of its subcategories.
⊢ (T ∈ Cat → T ∈ (SubCat ‘T))
Theorem	obsubc2 11305	The objects of a subcategory are a subset of those of the supercategory. JFM CAT2 th. 11 .
⊢ O1 = dom (id ‘T)    &   ⊢ O2 = dom (id ‘U)    ⇒   ⊢ (U ∈ (SubCat ‘T) → O2 ⊆ O1)
Theorem	idsubc 11306	The identity function of a subcategory is a subset of the identity function of the supercategory.
⊢ I1 = (id ‘T)    &   ⊢ I2 = (id ‘U)    ⇒   ⊢ (U ∈ (SubCat ‘T) → I2 ⊆ I1)
Theorem	domsubc 11307	The domain function of a subcategory is a subset of the domain function of the supercategory.
⊢ D1 = (dom ‘T)    &   ⊢ D2 = (dom ‘U)    ⇒   ⊢ (U ∈ (SubCat ‘T) → D2 ⊆ D1)
Theorem	codsubc 11308	The codomain function of a subcategory is a subset of the codomain function of the supercategory.
⊢ C1 = (cod ‘T)    &   ⊢ C2 = (cod ‘U)    ⇒   ⊢ (U ∈ (SubCat ‘T) → C2 ⊆ C1)
Theorem	subctct 11309	A subcategory is a category.
⊢ (U ∈ (SubCat ‘T) → U ∈ Cat)
Theorem	morsubc 11310	The morphisms of a subcategory are a subset of those of the supercategory.
⊢ M1 = dom (dom ‘T)    &   ⊢ M2 = dom (dom ‘U)    ⇒   ⊢ (U ∈ (SubCat ‘T) → M2 ⊆ M1)
Theorem	cmpsubc 11311	The composition law of a subcategory is a subset of the composition law of the supercategory.
⊢ Ro1 = (o ‘T)    &   ⊢ Ro2 = (o ‘U)    ⇒   ⊢ (U ∈ (SubCat ‘T) → Ro2 ⊆ Ro1)
Theorem	idsubidsup 11312	The identity of an an objet of the subcategory equals the identity of the object in the supercategory.
⊢ I1 = (id ‘T)    &   ⊢ I2 = (id ‘U)    &   ⊢ O2 = dom (id ‘U)    ⇒   ⊢ (U ∈ (SubCat ‘T) → ∀x ∈ O2 (I2 ‘x) = (I1 ‘x))
Theorem	idsubfun 11313	The identity restricted to the morphism of a subcategory U is a functor from the subcategory to the supercategory. It is called the inclusion functor. JFM CAT2 th. 19.
⊢ M = dom (dom ‘U)    ⇒   ⊢ (U ∈ (SubCat ‘T) → (I ↾ M) ∈ (Func ‘<.U, T>.))
Theorem	infemb 11314	The inclusion functor is an embedding.
⊢ M1 = dom (dom ‘T)    &   ⊢ M2 = dom (dom ‘U)    ⇒   ⊢ (U ∈ (SubCat ‘T) → (I ↾ M2):M2–1-1→M1)
Tarski's classes and ranks
Syntax	csubcl 11315	The class of subset-closed classes.
class Subcl
Syntax	ctarski 11316	The class of Tarski classes.
class Tarski
Definition	df-subcl 11317	( Define the class of all the subset-closed sets. )
⊢ Subcl = {x∣∀y∀z((y ∈ x ⋀ z ⊆ y) → z ∈ x)}
Planar incidence geometry
Syntax	cplig 11318	Extend class notation with the class of all planar incidence geometries.
class Plig
Definition	df-plig 11319	Planar incidence geometry. I use Hilbert's axioms adapted to planar geometry. ∈ is the incidence relation. I could take a generic incidence relation but I'm lazy and I'm not sure the gain is worth the extra work. Much of what follows is directly borrowed from Aitken. http://public.csusm.edu/aitken_html/m410/betweenness.pdf
⊢ Plig = {x∣(∀a ∈ ∪x∀b ∈ ∪x(a ≠ b → ∃!l ∈ x (a ∈ l ⋀ b ∈ l)) ⋀ ∀l ∈ x ∃a ∈ ∪x∃b ∈ ∪x(a ≠ b ⋀ a ∈ l ⋀ b ∈ l) ⋀ ∃a ∈ ∪x∃b ∈ ∪x∃c ∈ ∪x∀l ∈ x ¬ (a ∈ l ⋀ b ∈ l ⋀ c ∈ l))}
Theorem	isplig 11320	The predicate " is a planar incidence geometry ".
⊢ P = ∪L    ⇒   ⊢ (L ∈ A → (L ∈ Plig ↔ (∀a ∈ P ∀b ∈ P (a ≠ b → ∃!l ∈ L (a ∈ l ⋀ b ∈ l)) ⋀ ∀l ∈ L ∃a ∈ P ∃b ∈ P (a ≠ b ⋀ a ∈ l ⋀ b ∈ l) ⋀ ∃a ∈ P ∃b ∈ P ∃c ∈ P ∀l ∈ L ¬ (a ∈ l ⋀ b ∈ l ⋀ c ∈ l))))
Theorem	efp 11321	Euclid's first postulate. There is a unique line passing through two distinct points.
⊢ P = ∪L    ⇒   ⊢ (L ∈ Plig → ∀a ∈ P ∀b ∈ P (a ≠ b → ∃!l ∈ L (a ∈ l ⋀ b ∈ l)))
Theorem	efp2 11322	Euclid's first postulate. There is a unique line passing through two distinct points.
⊢ P = ∪L    ⇒   ⊢ ((L ∈ Plig ⋀ A ∈ P ⋀ B ∈ P) → (A ≠ B → ∃!l ∈ L (A ∈ l ⋀ B ∈ l)))
Theorem	l2p 11323	Any line has at least two distinct points.
⊢ P = ∪L    ⇒   ⊢ (L ∈ Plig → ∀l ∈ L ∃a ∈ P ∃b ∈ P (a ≠ b ⋀ a ∈ l ⋀ b ∈ l))
Theorem	tncp 11324	There exist three non colinear points.
⊢ P = ∪L    ⇒   ⊢ (L ∈ Plig → ∃a ∈ P ∃b ∈ P ∃c ∈ P ∀l ∈ L ¬ (a ∈ l ⋀ b ∈ l ⋀ c ∈ l))
Mathbox for Jeff Hankins
Miscellany
Theorem	3syld 11325	Triple syllogism deduction.
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (χ → θ))    &   ⊢ (φ → (θ → τ))    ⇒   ⊢ (φ → (ψ → τ))
Theorem	com45 11326	Commutation of antecedents. Swap 4th and 5th.
⊢ (φ → (ψ → (χ → (θ → (τ → η)))))    ⇒   ⊢ (φ → (ψ → (χ → (τ → (θ → η)))))
Theorem	com35 11327	Commutation of antecedents. Swap 3rd and 5th.
⊢ (φ → (ψ → (χ → (θ → (τ → η)))))    ⇒   ⊢ (φ → (ψ → (τ → (θ → (χ → η)))))
Theorem	com25 11328	Commutation of antecedents. Swap 2nd and 5th.
⊢ (φ → (ψ → (χ → (θ → (τ → η)))))    ⇒   ⊢ (φ → (τ → (χ → (θ → (ψ → η)))))
Theorem	com15 11329	Commutation of antecedents. Swap 1st and 5th.
⊢ (φ → (ψ → (χ → (θ → (τ → η)))))    ⇒   ⊢ (τ → (ψ → (χ → (θ → (φ → η)))))
Theorem	com5l 11330	Commutation of antecedents. Rotate left.
⊢ (φ → (ψ → (χ → (θ → (τ → η)))))    ⇒   ⊢ (ψ → (χ → (θ → (τ → (φ → η)))))
Theorem	com52l 11331	Commutation of antecedents. Rotate left twice.
⊢ (φ → (ψ → (χ → (θ → (τ → η)))))    ⇒   ⊢ (χ → (θ → (τ → (φ → (ψ → η)))))
Theorem	com52r 11332	Commutation of antecedents. Rotate right twice.
⊢ (φ → (ψ → (χ → (θ → (τ → η)))))    ⇒   ⊢ (θ → (τ → (φ → (ψ → (χ → η)))))
Theorem	a1i12 11333	Add two antecedents to a wff.
⊢ χ    ⇒   ⊢ (φ → (ψ → χ))
Theorem	a1i13 11334	Add two antecedents to a wff.
⊢ (ψ → θ)    ⇒   ⊢ (φ → (ψ → (χ → θ)))
Theorem	a1i4 11335	Add an antecedent to a wff.
⊢ (φ → (ψ → (χ → τ)))    ⇒   ⊢ (φ → (ψ → (χ → (θ → τ))))
Theorem	a1i14 11336	Add two antecedents to a wff.
⊢ (ψ → (χ → τ))    ⇒   ⊢ (φ → (ψ → (χ → (θ → τ))))
Theorem	a1i24 11337	Add two antecedents to a wff.
⊢ (φ → (χ → τ))    ⇒   ⊢ (φ → (ψ → (χ → (θ → τ))))
Theorem	a1i34 11338	Add two antecedents to a wff.
⊢ (φ → (ψ → τ))    ⇒   ⊢ (φ → (ψ → (χ → (θ → τ))))
Theorem	impbid3 11339	A variation on impbid 519.
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (¬ ψ → ¬ χ))    ⇒   ⊢ (φ → (ψ ↔ χ))
Theorem	ancomd 11340	Commutation of conjuncts in consequent.
⊢ (φ → (ψ ⋀ χ))    ⇒   ⊢ (φ → (χ ⋀ ψ))
Theorem	jca31 11341	Join three consequents.
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    ⇒   ⊢ (φ → ((ψ ⋀ χ) ⋀ θ))
Theorem	jca32 11342	Join three consequents.
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    ⇒   ⊢ (φ → (ψ ⋀ (χ ⋀ θ)))
Theorem	imp5a 11343	An importation inference.
⊢ (φ → (ψ → (χ → (θ → (τ → η)))))    ⇒   ⊢ (φ → (ψ → (χ → ((θ ⋀ τ) → η))))
Theorem	imp5d 11344	An importation inference.
⊢ (φ → (ψ → (χ → (θ → (τ → η)))))    ⇒   ⊢ (((φ ⋀ ψ) ⋀ χ) → ((θ ⋀ τ) → η))
Theorem	imp5g 11345	An importation inference.
⊢ (φ → (ψ → (χ → (θ → (τ → η)))))    ⇒   ⊢ ((φ ⋀ ψ) → (((χ ⋀ θ) ⋀ τ) → η))
Theorem	imp55 11346	An importation inference.
⊢ (φ → (ψ → (χ → (θ → (τ → η)))))    ⇒   ⊢ (((φ ⋀ (ψ ⋀ (χ ⋀ θ))) ⋀ τ) → η)
Theorem	imp511 11347	An importation inference.
⊢ (φ → (ψ → (χ → (θ → (τ → η)))))    ⇒   ⊢ ((φ ⋀ ((ψ ⋀ (χ ⋀ θ)) ⋀ τ)) → η)
Theorem	exp5c 11348	An exportation inference.
⊢ (φ → ((ψ ⋀ χ) → ((θ ⋀ τ) → η)))    ⇒   ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))
Theorem	exp5d 11349	An exportation inference.
⊢ (((φ ⋀ ψ) ⋀ χ) → ((θ ⋀ τ) → η))    ⇒   ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))
Theorem	exp5g 11350	An exportation inference.
⊢ ((φ ⋀ ψ) → (((χ ⋀ θ) ⋀ τ) → η))    ⇒   ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))
Theorem	exp5j 11351	An exportation inference.
⊢ (φ → ((((ψ ⋀ χ) ⋀ θ) ⋀ τ) → η))    ⇒   ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))
Theorem	exp5k 11352	An exportation inference.
⊢ (φ → (((ψ ⋀ (χ ⋀ θ)) ⋀ τ) → η))    ⇒   ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))
Theorem	exp5l 11353	An exportation inference.
⊢ (φ → (((ψ ⋀ χ) ⋀ (θ ⋀ τ)) → η))    ⇒   ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))
Theorem	exp53 11354	An exportation inference.
⊢ ((((φ ⋀ ψ) ⋀ (χ ⋀ θ)) ⋀ τ) → η)    ⇒   ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))
Theorem	exp56 11355	An exportation inference.
⊢ ((((φ ⋀ ψ) ⋀ χ) ⋀ (θ ⋀ τ)) → η)    ⇒   ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))
Theorem	exp58 11356	An exportation inference.
⊢ (((φ ⋀ ψ) ⋀ ((χ ⋀ θ) ⋀ τ)) → η)    ⇒   ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))
Theorem	exp510 11357	An exportation inference.
⊢ ((φ ⋀ (((ψ ⋀ χ) ⋀ θ) ⋀ τ)) → η)    ⇒   ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))
Theorem	exp511 11358	An exportation inference.
⊢ ((φ ⋀ ((ψ ⋀ (χ ⋀ θ)) ⋀ τ)) → η)    ⇒   ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))
Theorem	exp512 11359	An exportation inference.
⊢ ((φ ⋀ ((ψ ⋀ χ) ⋀ (θ ⋀ τ))) → η)    ⇒   ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))
Theorem	impr 11360	Import a wff into a right conjunct.
⊢ ((φ ⋀ ψ) → (χ → θ))    ⇒   ⊢ ((φ ⋀ (ψ ⋀ χ)) → θ)
Theorem	expl 11361	Export a wff from a left conjunct.
⊢ (((φ ⋀ ψ) ⋀ χ) → θ)    ⇒   ⊢ (φ → ((ψ ⋀ χ) → θ))
Theorem	expr 11362	Export a wff from a right conjunct.
⊢ ((φ ⋀ (ψ ⋀ χ)) → θ)    ⇒   ⊢ ((φ ⋀ ψ) → (χ → θ))
Theorem	simplll 11363	Simplification of a conjunction.
⊢ ((((φ ⋀ ψ) ⋀ χ) ⋀ θ) → φ)
Theorem	simpllr 11364	Simplification of a conjunction.
⊢ ((((φ ⋀ ψ) ⋀ χ) ⋀ θ) → ψ)
Theorem	simplrl 11365	Simplification of a conjunction.
⊢ (((φ ⋀ (ψ ⋀ χ)) ⋀ θ) → ψ)
Theorem	simplrr 11366	Simplification of a conjunction.
⊢ (((φ ⋀ (ψ ⋀ χ)) ⋀ θ) → χ)
Theorem	simprll 11367	Simplification of a conjunction.
⊢ ((φ ⋀ ((ψ ⋀ χ) ⋀ θ)) → ψ)
Theorem	simprlr 11368	Simplification of a conjunction.
⊢ ((φ ⋀ ((ψ ⋀ χ) ⋀ θ)) → χ)
Theorem	simprrl 11369	Simplification of a conjunction.
⊢ ((φ ⋀ (ψ ⋀ (χ ⋀ θ))) → χ)
Theorem	simprrr 11370	Simplification of a conjunction.
⊢ ((φ ⋀ (ψ ⋀ (χ ⋀ θ))) → θ)
Theorem	sylan31c 11371	A syllogism inference combined with contraction.
⊢ (τ → φ)    &   ⊢ (τ → ψ)    &   ⊢ (τ → χ)    &   ⊢ (((φ ⋀ ψ) ⋀ χ) → θ)    ⇒   ⊢ (τ → θ)
Theorem	sylan32c 11372	A syllogism inference combined with contraction.
⊢ (τ → φ)    &   ⊢ (τ → ψ)    &   ⊢ (τ → χ)    &   ⊢ ((φ ⋀ (ψ ⋀ χ)) → θ)    ⇒   ⊢ (τ → θ)
Theorem	mtand 11373	A modus tollens deduction.
⊢ (φ → ¬ χ)    &   ⊢ ((φ ⋀ ψ) → χ)    ⇒   ⊢ (φ → ¬ ψ)
Theorem	mtord 11374	A modus tollens deduction involving disjunction.
⊢ (φ → ¬ χ)    &   ⊢ (φ → ¬ θ)    &   ⊢ (φ → (ψ → (χ ⋁ θ)))    ⇒   ⊢ (φ → ¬ ψ)
Theorem	3anim1i 11375	Add two conjuncts to antecedent and consequent.
⊢ (φ → ψ)    ⇒   ⊢ ((φ ⋀ χ ⋀ θ) → (ψ ⋀ χ ⋀ θ))
Theorem	3anim3i 11376	Add two conjuncts to antecedent and consequent.
⊢ (φ → ψ)    ⇒   ⊢ ((χ ⋀ θ ⋀ φ) → (χ ⋀ θ ⋀ ψ))
Theorem	3simpl1 11377	Simplification rule.
⊢ (((φ ⋀ ψ ⋀ χ) ⋀ θ) → φ)
Theorem	3simpl2 11378	Simplification rule.
⊢ (((φ ⋀ ψ ⋀ χ) ⋀ θ) → ψ)
Theorem	3simpl3 11379	Simplification rule.
⊢ (((φ ⋀ ψ ⋀ χ) ⋀ θ) → χ)
Theorem	3simpr1 11380	Simplification rule.
⊢ ((φ ⋀ (ψ ⋀ χ ⋀ θ)) → ψ)
Theorem	3simpr2 11381	Simplification rule.
⊢ ((φ ⋀ (ψ ⋀ χ ⋀ θ)) → χ)
Theorem	3simpr3 11382	Simplification rule.
⊢ ((φ ⋀ (ψ ⋀ χ ⋀ θ)) → θ)
Theorem	3com12d 11383	Commutation in consequent. Swap 1st and 2nd.
⊢ (φ → (ψ ⋀ χ ⋀ θ))    ⇒   ⊢ (φ → (χ ⋀ ψ ⋀ θ))
Theorem	imp5p 11384	A triple importation inference.
⊢ (φ → (ψ → (χ → (θ → (τ → η)))))    ⇒   ⊢ (φ → (ψ → ((χ ⋀ θ ⋀ τ) → η)))
Theorem	imp5q 11385	A triple importation inference.
⊢ (φ → (ψ → (χ → (θ → (τ → η)))))    ⇒   ⊢ ((φ ⋀ ψ) → ((χ ⋀ θ ⋀ τ) → η))
Theorem	exp5o 11386	A triple exportation inference.
⊢ ((φ ⋀ ψ ⋀ χ) → ((θ ⋀ τ) → η))    ⇒   ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))
Theorem	exp516 11387	A triple exportation inference.
⊢ (((φ ⋀ (ψ ⋀ χ ⋀ θ)) ⋀ τ) → η)    ⇒   ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))
Theorem	exp520 11388	A triple exportation inference.
⊢ (((φ ⋀ ψ ⋀ χ) ⋀ (θ ⋀ τ)) → η)    ⇒   ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))
Theorem	3jaao 11389	Inference conjoining and disjoining the antecedents of three implications.
⊢ (φ → (ψ → χ))    &   ⊢ (θ → (τ → χ))    &   ⊢ (η → (ζ → χ))    ⇒   ⊢ ((φ ⋀ θ ⋀ η) → ((ψ ⋁ τ ⋁ ζ) → χ))
Theorem	3anor 11390	Triple conjunction expressed in terms of triple disjunction.
⊢ ((φ ⋀ ψ ⋀ χ) ↔ ¬ (¬ φ ⋁ ¬ ψ ⋁ ¬ χ))
Theorem	3ianor 11391	Negated triple conjunction expressed in terms of triple disjunction.
⊢ (¬ (φ ⋀ ψ ⋀ χ) ↔ (¬ φ ⋁ ¬ ψ ⋁ ¬ χ))
Theorem	ecase13d 11392	Deduction for elimination by cases.
⊢ (φ → ¬ χ)    &   ⊢ (φ → ¬ θ)    &   ⊢ (φ → (χ ⋁ ψ ⋁ θ))    ⇒   ⊢ (φ → ψ)
Theorem	nexnoti 11393	Inference form of nexnot (future).
⊢ ¬ ∃xφ    ⇒   ⊢ ¬ φ
Theorem	r19.2zb 11394	A response to the notion that the condition A ≠ ∅ can be removed in r19.2z 2402. Interestingly enough, φ does not figure in the left-hand side.
⊢ (A ≠ ∅ ↔ (∀x ∈ A φ → ∃x ∈ A φ))
Theorem	eqeu 11395	A condition which implies existential uniqueness.
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ ((A ∈ B ⋀ ψ ⋀ ∀x(φ → x = A)) → ∃!xφ)
Theorem	subtr 11396	Transitivity of implicit substitution.
⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (y ∈ B → ∀x y ∈ B)    &   ⊢ (y ∈ Y → ∀x y ∈ Y)    &   ⊢ (y ∈ Z → ∀x y ∈ Z)    &   ⊢ (x = A → X = Y)    &   ⊢ (x = B → X = Z)    ⇒   ⊢ ((A ∈ C ⋀ B ∈ D) → (A = B → Y = Z))
Theorem	subtr2 11397	Transitivity of implicit substitution into a wff.
⊢ (y ∈ A → ∀x y ∈ A)    &   ⊢ (y ∈ B → ∀x y ∈ B)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (χ → ∀xχ)    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ (x = B → (φ ↔ χ))    ⇒   ⊢ ((A ∈ C ⋀ B ∈ D) → (A = B → (ψ ↔ χ)))
Theorem	cbvcsb 11398	Change bound variables in a class substitution. Interestingly, this does not require any bound variable conditions on A.
⊢ (z ∈ C → ∀y z ∈ C)    &   ⊢ (z ∈ D → ∀x z ∈ D)    &   ⊢ (x = y → C = D)    ⇒   ⊢ (A ∈ B → [A / x]C = [A / y]D)
Theorem	cbvsbc 11399	Change bound variables in a wff substitution.
⊢ (φ → ∀yφ)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (A ∈ B → ([A / x]φ ↔ [A / y]ψ))
Theorem	indif2 11400	Bring an intersection in and out of a class difference.
⊢ (A ∩ (B ∖ C)) = ((A ∩ B) ∖ C)