mmtheorems21 - 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 - 2001-2100 - Page 21 of 123

Type	Label	Description
Statement
Theorem	sbc5 2001	An equivalence for class substitution.
|- A e. V   =>   |- ([A / x]ph <-> E.x(x = A /\ ph))
Theorem	sbc6 2002	An equivalence for class substitution. (The proof was shortened by Eric Schmidt, 17-Jan-2007.)
|- A e. V   =>   |- ([A / x]ph <-> A.x(x = A -> ph))
Theorem	sbc7g 2003	An equivalence for class substitution in the spirit of df-clab 1506. Note that x and A don't have to be distinct.
|- (A e. B -> ([A / x]ph <-> E.y(y = A /\ [y / x]ph)))
Theorem	sbc8g 2004	This is the closest we can get to df-sbc 1987 if we start from dfsbcq 1988 (see its comments).
|- (A e. B -> ([A / x]ph <-> A e. {x | ph}))
Theorem	cbvsbcv 2005	Change the bound variable of a class substitution using implicit substitution.
|- (x = y -> (ph <-> ps))   =>   |- (A e. B -> ([A / x]ph <-> [A / y]ps))
Theorem	sbc2or 2006	The disjunction of two equivalences for class substitution does not require a class existence hypothesis. This theorem tells us that there are only 2 possibilities for defining [A / x]ph behavior at proper classes (given a specific A), which is interesting since dfsbcq 1988 (from which it is derived) does not say anything obvious about that.
|- (([A / x]ph <-> E.x(x = A /\ ph)) \/ ([A / x]ph <-> A.x(x = A -> ph)))
Theorem	sbciegft 2007	Conversion of implicit substitution to explicit class substitution, using a bound-variable hypothesis instead of distinct variables. (Closed theorem version of sbciegf 2008.)
|- ((A e. B /\ A.x(ps -> A.xps) /\ A.x(x = A -> (ph <-> ps))) -> ([A / x]ph <-> ps))
Theorem	sbciegf 2008	Conversion of implicit substitution to explicit class substitution.
|- (A e. B -> (ps -> A.xps))   &   |- (x = A -> (ph <-> ps))   =>   |- (A e. B -> ([A / x]ph <-> ps))
Theorem	sbcieg 2009	Conversion of implicit substitution to explicit class substitution.
|- (x = A -> (ph <-> ps))   =>   |- (A e. B -> ([A / x]ph <-> ps))
Theorem	sbcie 2010	Conversion of implicit substitution to explicit class substitution.
|- A e. V   &   |- (x = A -> (ph <-> ps))   =>   |- ([A / x]ph <-> ps)
Theorem	elrabsf 2011	Membership in a restricted class abstraction, expressed with explicit class substitution. (The variation elrabf 1950 has implicit substitution). The hypothesis specifies that x must not be a free variable in B.
|- (y e. B -> A.x y e. B)   =>   |- (A e. {x e. B | ph} <-> (A e. B /\ [A / x]ph))
Theorem	elabs2 2012	Membership in a class abstraction, expressed in terms of class substitution. Theorem 6.13 of [Quine] p. 44.
|- (A e. {x | ph} <-> (A e. V /\ [A / x]ph))
Theorem	elabsg 2013	Membership in a class abstraction, expressed in terms of class substitution. Conveniently, this theorem has no distinct variable restrictions. Except for the antecedent, this theorem is "almost" like df-sbc 1987 but was proved using only dfsbcq 1988 as its starting point (making no other reference to df-sbc 1987). We prefer not to make direct reference to df-sbc 1987 (i.e. commit to it) since its behavior at proper classes is at odds with Quine, whereas dfsbcq 1988 is not. (Quine's class substitution cannot be expressed in closed form.) This theorem serves as a weaker Quine-compatible substitute for df-sbc 1987.
|- (A e. B -> (A e. {x | ph} <-> [A / x]ph))
Theorem	elabs 2014	Membership in a class abstraction, expressed in terms of class substitution.
|- A e. V   =>   |- (A e. {x | ph} <-> [A / x]ph)
Theorem	cbvralsv 2015	Change bound variable by using a substitution.
|- (A.x e. A ph <-> A.y e. A [y / x]ph)
Theorem	cbvrexsv 2016	Change bound variable by using a substitution.
|- (E.x e. A ph <-> E.y e. A [y / x]ph)
Theorem	sbcng 2017	Move negation in and out of class substitution.
|- (A e. B -> ([A / x] -. ph <-> -. [A / x]ph))
Theorem	sbcimg 2018	Distribution of class substitution over implication.
|- (A e. B -> ([A / x](ph -> ps) <-> ([A / x]ph -> [A / x]ps)))
Theorem	sbcang 2019	Distribution of class substitution over conjunction.
|- (A e. B -> ([A / x](ph /\ ps) <-> ([A / x]ph /\ [A / x]ps)))
Theorem	sbcorg 2020	Distribution of class substitution over disjunction.
|- (A e. B -> ([A / x](ph \/ ps) <-> ([A / x]ph \/ [A / x]ps)))
Theorem	sbcbidig 2021	Distribution of class substitution over biconditional. (Contributed by Raph Levien, 10-Apr-2004.)
|- (A e. B -> ([A / x](ph <-> ps) <-> ([A / x]ph <-> [A / x]ps)))
Theorem	sbcalg 2022	Move universal quantifier in and out of class substitution.
|- (A e. B -> ([A / y]A.xph <-> A.x[A / y]ph))
Theorem	sbcexg 2023	Move existential quantifier in and out of class substitution.
|- (A e. B -> ([A / y]E.xph <-> E.x[A / y]ph))
Theorem	sbcbid 2024	Formula-building deduction rule for class substitution.
|- (ph -> A.xph)   &   |- (ph -> (ps <-> ch))   =>   |- ((ph /\ A e. B) -> ([A / x]ps <-> [A / x]ch))
Theorem	sbcbidv 2025	Formula-building deduction rule for class substitution. (The proof was shortened by Eric Schmidt, 17-Jan-2007.)
|- (ph -> (ps <-> ch))   =>   |- ((ph /\ A e. B) -> ([A / x]ps <-> [A / x]ch))
Theorem	sbcbii 2026	Formula-building inference rule for class substitution.
|- (ph <-> ps)   =>   |- (A e. B -> ([A / x]ph <-> [A / x]ps))
Theorem	sbc3ang 2027	Distribution of class substitution over triple conjunction.
|- (A e. B -> ([A / x](ph /\ ps /\ ch) <-> ([A / x]ph /\ [A / x]ps /\ [A / x]ch)))
Theorem	sbcel1gv 2028	Class substitution into a membership relation.
|- (A e. C -> ([A / x]x e. B <-> A e. B))
Theorem	sbcel2gv 2029	Class substitution into a membership relation.
|- (B e. C -> ([B / x]A e. x <-> A e. B))
Theorem	sbcth2 2030	A substitution into a theorem.
|- (x e. B -> ph)   =>   |- (A e. B -> [A / x]ph)
Theorem	hbsbc1gd 2031	Deduction version of hbsbc1g 1993.
|- (ph -> A.xph)   &   |- (ph -> (y e. A -> A.x y e. A))   =>   |- ((ph /\ A e. B) -> ([A / x]ps -> A.x[A / x]ps))
Theorem	hbsbcgd 2032	Deduction version of hbsbcg 1996.
|- (ph -> A.xph)   &   |- (ph -> A.yph)   &   |- (ph -> (z e. A -> A.x z e. A))   &   |- (ph -> (ps -> A.xps))   =>   |- ((ph /\ A e. C) -> ([A / y]ps -> A.x[A / y]ps))
Theorem	sbc19.20dv 2033	Substitution analog of Theorem 19.20 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- ((ph /\ A e. B) -> ([A / x]ps -> [A / x]ch))
Theorem	sbcgf 2034	Substitution for a variable not free in a wff does not affect it.
|- (ph -> A.xph)   =>   |- (A e. B -> ([A / x]ph <-> ph))
Theorem	sbc19.21g 2035	Substitution for a variable not free in antecedent affects only the consequent.
|- (ph -> A.xph)   =>   |- (A e. B -> ([A / x](ph -> ps) <-> (ph -> [A / x]ps)))
Theorem	sbc2ie 2036	Conversion of implicit substitution to explicit class substitution.
|- A e. V   &   |- B e. V   &   |- ((x = A /\ y = B) -> (ph <-> ps))   =>   |- ([A / x][B / y]ph <-> ps)
Theorem	sbc2iedv 2037	Conversion of implicit substitution to explicit class substitution.
|- A e. V   &   |- B e. V   &   |- (ph -> ((x = A /\ y = B) -> (ps <-> ch)))   =>   |- (ph -> ([A / x][B / y]ps <-> ch))
Theorem	sbccomglem 2038	Lemma for sbccomg 2039.
Theorem	sbccomg 2039	Commutative law for double class substitution. (The proof was shortened by Eric Schmidt, 17-Jan-2007.)
|- ((A e. C /\ B e. D) -> ([A / x][B / y]ph <-> [B / y][A / x]ph))
Theorem	sbcralt 2040	Interchange class substitution and restricted quantifier. (Unnecessary distinct variable restrictions were removed by David Abernethy, 22-Feb-2010.)
|- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> ([A / x]A.y e. B ph <-> A.y e. B [A / x]ph))
Theorem	sbcrext 2041	Interchange class substitution and restricted existential quantifier. (Unnecessary distinct variable restrictions were removed by David Abernethy, 22-Feb-2010.)
|- (A.y(A e. C /\ A.z(z e. A -> A.y z e. A)) -> ([A / x]E.y e. B ph <-> E.y e. B [A / x]ph))
Theorem	sbcralgf 2042	Interchange class substitution and restricted quantifier.
|- (A.y A e. C -> (z e. A -> A.y z e. A))   =>   |- (A.y A e. C -> ([A / x]A.y e. B ph <-> A.y e. B [A / x]ph))
Theorem	sbcrexgf 2043	Interchange class substitution and restricted existential quantifier.
|- (A.y A e. C -> (z e. A -> A.y z e. A))   =>   |- (A.y A e. C -> ([A / x]E.y e. B ph <-> E.y e. B [A / x]ph))
Theorem	sbcralg 2044	Interchange class substitution and restricted quantifier.
|- (A e. C -> ([A / x]A.y e. B ph <-> A.y e. B [A / x]ph))
Theorem	sbcrexg 2045	Interchange class substitution and restricted existential quantifier.
|- (A e. C -> ([A / x]E.y e. B ph <-> E.y e. B [A / x]ph))
Theorem	sbcabel 2046	Interchange class substitution and class abstraction.
|- (z e. B -> A.x z e. B)   =>   |- (A e. C -> ([A / x]{y | ph} e. B <-> {y | [A / x]ph} e. B))
Theorem	ra4sbc 2047	Restricted quantifier version of Axiom 4 of [Mendelson] p. 69. This provides an axiom for a predicate calculus for a restricted domain. This theorem generalizes the unrestricted stdpc4 1222 and a4sbc 1990. See also ra4sbca 2048 and ra4csbela 2094.
|- (A e. B -> (A.x e. B ph -> [A / x]ph))
Theorem	ra4sbca 2048	Restricted quantifier version of Axiom 4 of [Mendelson] p. 69.
|- ((A e. B /\ A.x e. B ph) -> [A / x]ph)
Theorem	ra4esbca 2049	Existence form of ra4sbca 2048.
|- ((A e. B /\ [A / x]ph) -> E.x e. B ph)
Theorem	ra5 2050	Restricted quantifier version of Axiom 5 of [Mendelson] p. 69. This is an axiom of a predicate calculus for a restricted domain. Compare the unrestricted stdpc5 1094.
|- (ph -> A.xph)   =>   |- (A.x e. A (ph -> ps) -> (ph -> A.x e. A ps))
Proper substitution of classes for sets into classes
Syntax	csb 2051	Extend class notation to include the proper substitution of a class for a set into another class.
class [_A / x]_B
Definition	df-csb 2052	Define the proper substitution of a class for a set into another class. The underlined brackets distinguish it from the substitution into a wff, wsbc 1207, to prevent ambiguity. Theorem sbcel1g 2064 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2073 recreates substitution into a wff from this definition.
|- [_A / x]_B = {y | [A / x]y e. B}
Theorem	csbeq1 2053	Analog of dfsbcq 1988 for proper substitution into a class.
|- (A = B -> [_A / x]_C = [_B / x]_C)
Theorem	cbvcsbv 2054	Change the bound variable of a proper substitution into a class using implicit substitution.
|- (x = y -> B = C)   =>   |- (A e. D -> [_A / x]_B = [_A / y]_C)
Theorem	csbeq1d 2055	Equality deduction for proper substitution into a class.
|- (ph -> A = B)   =>   |- (ph -> [_A / x]_C = [_B / x]_C)
Theorem	csbid 2056	Analog of sbid 1221 for proper substitution into a class.
|- [_x / x]_A = A
Theorem	csbeq1a 2057	Equality theorem for proper substitution into a class.
|- (x = A -> B = [_A / x]_B)
Theorem	csbcog 2058	Composition law for chained substitutions into a class.
|- (A e. C -> [_A / y]_[_y / x]_B = [_A / x]_B)
Theorem	csbexg 2059	The existence of proper substitution into a class.
|- ((A e. C /\ A.x B e. D) -> [_A / x]_B e. V)
Theorem	csbex 2060	The existence of proper substitution into a class.
|- A e. V   &   |- B e. V   =>   |- [_A / x]_B e. V
Theorem	csbconstgf 2061	Substitution doesn't affect a constant B (in which x is not free).
|- (y e. B -> A.x y e. B)   =>   |- (A e. C -> [_A / x]_B = B)
Theorem	sbcel12g 2062	Distribute proper substitution through a membership relation.
|- (A e. D -> ([A / x]B e. C <-> [_A / x]_B e. [_A / x]_C))
Theorem	sbceqdig 2063	Distribute proper substitution through an equality relation.
|- (A e. D -> ([A / x]B = C <-> [_A / x]_B = [_A / x]_C))
Theorem	sbcel1g 2064	Move proper substitution in and out of a membership relation. Note that the scope of [A / x] is the wff B e. C, whereas the scope of [_A / x]_ is the class B.
|- (A e. D -> ([A / x]B e. C <-> [_A / x]_B e. C))
Theorem	sbceq1dig 2065	Move proper substitution to first argument of an equality.
|- (A e. D -> ([A / x]B = C <-> [_A / x]_B = C))
Theorem	sbcel2g 2066	Move proper substitution in and out of a membership relation.
|- (A e. D -> ([A / x]B e. C <-> B e. [_A / x]_C))
Theorem	sbceq2dig 2067	Move proper substitution to second argument of an equality.
|- (A e. D -> ([A / x]B = C <-> B = [_A / x]_C))
Theorem	csbcomg 2068	Commutative law for double substitution into a class.
|- ((A e. R /\ B e. S) -> [_A / x]_[_B / y]_C = [_B / y]_[_A / x]_C)
Theorem	csbeq2d 2069	Formula-building deduction rule for class substitution.
|- (ph -> A.xph)   &   |- (ph -> B = C)   =>   |- ((ph /\ A e. D) -> [_A / x]_B = [_A / x]_C)
Theorem	csbeq2dv 2070	Formula-building deduction rule for class substitution.
|- (ph -> B = C)   =>   |- ((ph /\ A e. D) -> [_A / x]_B = [_A / x]_C)
Theorem	csbeq2i 2071	Formula-building inference rule for class substitution.
|- B = C   =>   |- (A e. D -> [_A / x]_B = [_A / x]_C)
Theorem	csbvarg 2072	The proper substitution of a class for set variable results in the class (if the class exists).
|- (A e. B -> [_A / x]_x = A)
Theorem	sbccsbg 2073	Substitution into a wff expressed in terms of substitution into a class.
|- (A e. B -> ([A / x]ph <-> y e. [_A / x]_{y | ph}))
Theorem	sbccsb2g 2074	Substitution into a wff expressed in using substitution into a class.
|- (A e. B -> ([A / x]ph <-> A e. [_A / x]_{x | ph}))
Theorem	hbcsb1g 2075	Bound-variable hypothesis builder for substitution into a class.
|- (y e. A -> A.x y e. A)   =>   |- (A e. C -> (y e. [_A / x]_B -> A.x y e. [_A / x]_B))
Theorem	hbcsb1 2076	Bound-variable hypothesis builder for substitution into a class.
|- A e. V   &   |- (y e. A -> A.x y e. A)   =>   |- (y e. [_A / x]_B -> A.x y e. [_A / x]_B)
Theorem	hbcsbg 2077	Bound-variable hypothesis builder for substitution into a class.
|- (z e. A -> A.x z e. A)   &   |- (z e. B -> A.x z e. B)   =>   |- (A e. C -> (z e. [_A / y]_B -> A.x z e. [_A / y]_B))
Theorem	hbcsb1gd 2078	Deduction version of hbcsb1g 2075.
|- (ph -> A.xph)   &   |- (ph -> (y e. A -> A.x y e. A))   =>   |- ((ph /\ A e. C) -> (y e. [_A / x]_B -> A.x y e. [_A / x]_B))
Theorem	hbcsbgd 2079	Deduction version of hbcsbg 2077.
|- (ph -> A.xph)   &   |- (ph -> A.yph)   &   |- (ph -> (z e. A -> A.x z e. A))   &   |- (ph -> (z e. B -> A.x z e. B))   =>   |- ((ph /\ A e. C) -> (z e. [_A / y]_B -> A.x z e. [_A / y]_B))
Theorem	csbhypf 2080	Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf 1985 for class substitution version.
|- (z e. A -> A.x z e. A)   &   |- (z e. C -> A.x z e. C)   &   |- (x = A -> B = C)   =>   |- (y = A -> [_y / x]_B = C)
Theorem	csbiegft 2081	Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 2083.)
|- ((A e. D /\ A.xA.y(y e. C -> A.x y e. C) /\ A.x(x = A -> B = C)) -> [_A / x]_B = C)
Theorem	csbieb 2082	Bidirectional conversion between an implicit class substitution hypothesis x = A -> B = C and its explicit substitution equivalent.
|- A e. V   &   |- (y e. C -> A.x y e. C)   =>   |- (A.x(x = A -> B = C) <-> [_A / x]_B = C)
Theorem	csbiegf 2083	Conversion of implicit substitution to explicit substitution into a class.
|- (A e. D -> (y e. C -> A.x y e. C))   &   |- (x = A -> B = C)   =>   |- (A e. D -> [_A / x]_B = C)
Theorem	csbief 2084	Conversion of implicit substitution to explicit substitution into a class.
|- A e. V   &   |- (y e. C -> A.x y e. C)   &   |- (x = A -> B = C)   =>   |- [_A / x]_B = C
Theorem	csbie2t 2085	Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 2086).
|- A e. V   &   |- B e. V   =>   |- (A.xA.y((x = A /\ y = B) -> C = D) -> [_A / x]_[_B / y]_C = D)
Theorem	csbie2 2086	Conversion of implicit substitution to explicit substitution into a class.
|- A e. V   &   |- B e. V   &   |- ((x = A /\ y = B) -> C = D)   =>   |- [_A / x]_[_B / y]_C = D
Theorem	csbnestglem 2087	Lemma for csbnestg 2088.
Theorem	csbnestg 2088	Nest the composition of two substitutions.
|- ((A e. R /\ A.x B e. S) -> [_A / x]_[_B / y]_C = [_[_A / x]_B / y]_C)
Theorem	csbnest1g 2089	Nest the composition of two substitutions.
|- ((A e. R /\ A.x B e. S) -> [_A / x]_[_B / x]_C = [_[_A / x]_B / x]_C)
Theorem	sbcnestg 2090	Nest the composition of two substitutions.
|- ((A e. R /\ A.x B e. S) -> ([A / x][B / y]ph <-> [[_A / x]_B / y]ph))
Theorem	csbidmg 2091	Idempotent law for class substitutions.
|- (A e. C -> [_A / x]_[_A / x]_B = [_A / x]_B)
Theorem	csbco3g 2092	Composition of two class substitutions.
|- (x = A -> B = D)   =>   |- ((A e. R /\ A.x B e. S) -> [_A / x]_[_B / y]_C = [_D / y]_C)
Theorem	sbcco3g 2093	Composition of two substitutions.
|- (x = A -> B = C)   =>   |- ((A e. R /\ A.x B e. S) -> ([A / x][B / y]ph <-> [C / y]ph))
Theorem	ra4csbela 2094	Special case related to ra4sbc 2047. (The proof was shortened by Eric Schmidt, 17-Jan-2007.)
|- ((A e. B /\ A.x e. B C e. D) -> [_A / x]_C e. D)
Theorem	csbabg 2095	Move substitution into a class abstraction.
|- (A e. B -> [_A / x]_{y | ph} = {y | [A / x]ph})
Define basic set operations and relations
Syntax	cdif 2096	Extend class notation to include class difference (read: "A minus B").
class (A \ B)
Syntax	cun 2097	Extend class notation to include union of two classes (read: "A union B").
class (A u. B)
Syntax	cin 2098	Extend class notation to include the intersection of two classes (read: "A intersect B").
class (A i^i B)
Syntax	wss 2099	Extend wff notation to include the subclass relation. This is read "A is a subclass of B" or "B includes A." When A exists as a set, it is also read "A is a subset of B."
wff A (_ B
Syntax	wpss 2100	Extend wff notation with proper subclass relation.
wff A (. B