HomeHome Intuitionistic Logic Explorer
Theorem List (p. 22 of 116)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 2101-2200   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremeqeq12i 2101 A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  A  =  B   &    |-  C  =  D   =>    |-  ( A  =  C  <->  B  =  D )
 
Theoremeqeq12d 2102 A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  C  =  D )   =>    |-  ( ph  ->  ( A  =  C  <->  B  =  D ) )
 
Theoremeqeqan12d 2103 A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ps  ->  C  =  D )   =>    |-  ( ( ph  /\ 
 ps )  ->  ( A  =  C  <->  B  =  D ) )
 
Theoremeqeqan12rd 2104 A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ps  ->  C  =  D )   =>    |-  ( ( ps 
 /\  ph )  ->  ( A  =  C  <->  B  =  D ) )
 
Theoremeqtr 2105 Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13. (Contributed by NM, 25-Jan-2004.)
 |-  ( ( A  =  B  /\  B  =  C )  ->  A  =  C )
 
Theoremeqtr2 2106 A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  ( ( A  =  B  /\  A  =  C )  ->  B  =  C )
 
Theoremeqtr3 2107 A transitive law for class equality. (Contributed by NM, 20-May-2005.)
 |-  ( ( A  =  C  /\  B  =  C )  ->  A  =  B )
 
Theoremeqtri 2108 An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
 |-  A  =  B   &    |-  B  =  C   =>    |-  A  =  C
 
Theoremeqtr2i 2109 An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
 |-  A  =  B   &    |-  B  =  C   =>    |-  C  =  A
 
Theoremeqtr3i 2110 An equality transitivity inference. (Contributed by NM, 6-May-1994.)
 |-  A  =  B   &    |-  A  =  C   =>    |-  B  =  C
 
Theoremeqtr4i 2111 An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
 |-  A  =  B   &    |-  C  =  B   =>    |-  A  =  C
 
Theorem3eqtri 2112 An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)
 |-  A  =  B   &    |-  B  =  C   &    |-  C  =  D   =>    |-  A  =  D
 
Theorem3eqtrri 2113 An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  A  =  B   &    |-  B  =  C   &    |-  C  =  D   =>    |-  D  =  A
 
Theorem3eqtr2i 2114 An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.)
 |-  A  =  B   &    |-  C  =  B   &    |-  C  =  D   =>    |-  A  =  D
 
Theorem3eqtr2ri 2115 An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  A  =  B   &    |-  C  =  B   &    |-  C  =  D   =>    |-  D  =  A
 
Theorem3eqtr3i 2116 An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  A  =  B   &    |-  A  =  C   &    |-  B  =  D   =>    |-  C  =  D
 
Theorem3eqtr3ri 2117 An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)
 |-  A  =  B   &    |-  A  =  C   &    |-  B  =  D   =>    |-  D  =  C
 
Theorem3eqtr4i 2118 An inference from three chained equalities. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  A  =  B   &    |-  C  =  A   &    |-  D  =  B   =>    |-  C  =  D
 
Theorem3eqtr4ri 2119 An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  A  =  B   &    |-  C  =  A   &    |-  D  =  B   =>    |-  D  =  C
 
Theoremeqtrd 2120 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  B  =  C )   =>    |-  ( ph  ->  A  =  C )
 
Theoremeqtr2d 2121 An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  B  =  C )   =>    |-  ( ph  ->  C  =  A )
 
Theoremeqtr3d 2122 An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  A  =  C )   =>    |-  ( ph  ->  B  =  C )
 
Theoremeqtr4d 2123 An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  C  =  B )   =>    |-  ( ph  ->  A  =  C )
 
Theorem3eqtrd 2124 A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  B  =  C )   &    |-  ( ph  ->  C  =  D )   =>    |-  ( ph  ->  A  =  D )
 
Theorem3eqtrrd 2125 A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  B  =  C )   &    |-  ( ph  ->  C  =  D )   =>    |-  ( ph  ->  D  =  A )
 
Theorem3eqtr2d 2126 A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  C  =  B )   &    |-  ( ph  ->  C  =  D )   =>    |-  ( ph  ->  A  =  D )
 
Theorem3eqtr2rd 2127 A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  C  =  B )   &    |-  ( ph  ->  C  =  D )   =>    |-  ( ph  ->  D  =  A )
 
Theorem3eqtr3d 2128 A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  A  =  C )   &    |-  ( ph  ->  B  =  D )   =>    |-  ( ph  ->  C  =  D )
 
Theorem3eqtr3rd 2129 A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  A  =  C )   &    |-  ( ph  ->  B  =  D )   =>    |-  ( ph  ->  D  =  C )
 
Theorem3eqtr4d 2130 A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  C  =  A )   &    |-  ( ph  ->  D  =  B )   =>    |-  ( ph  ->  C  =  D )
 
Theorem3eqtr4rd 2131 A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  C  =  A )   &    |-  ( ph  ->  D  =  B )   =>    |-  ( ph  ->  D  =  C )
 
Theoremsyl5eq 2132 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
 |-  A  =  B   &    |-  ( ph  ->  B  =  C )   =>    |-  ( ph  ->  A  =  C )
 
Theoremsyl5req 2133 An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
 |-  A  =  B   &    |-  ( ph  ->  B  =  C )   =>    |-  ( ph  ->  C  =  A )
 
Theoremsyl5eqr 2134 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
 |-  B  =  A   &    |-  ( ph  ->  B  =  C )   =>    |-  ( ph  ->  A  =  C )
 
Theoremsyl5reqr 2135 An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
 |-  B  =  A   &    |-  ( ph  ->  B  =  C )   =>    |-  ( ph  ->  C  =  A )
 
Theoremsyl6eq 2136 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
 |-  ( ph  ->  A  =  B )   &    |-  B  =  C   =>    |-  ( ph  ->  A  =  C )
 
Theoremsyl6req 2137 An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
 |-  ( ph  ->  A  =  B )   &    |-  B  =  C   =>    |-  ( ph  ->  C  =  A )
 
Theoremsyl6eqr 2138 An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
 |-  ( ph  ->  A  =  B )   &    |-  C  =  B   =>    |-  ( ph  ->  A  =  C )
 
Theoremsyl6reqr 2139 An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
 |-  ( ph  ->  A  =  B )   &    |-  C  =  B   =>    |-  ( ph  ->  C  =  A )
 
Theoremsylan9eq 2140 An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ps  ->  B  =  C )   =>    |-  ( ( ph  /\ 
 ps )  ->  A  =  C )
 
Theoremsylan9req 2141 An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.)
 |-  ( ph  ->  B  =  A )   &    |-  ( ps  ->  B  =  C )   =>    |-  ( ( ph  /\ 
 ps )  ->  A  =  C )
 
Theoremsylan9eqr 2142 An equality transitivity deduction. (Contributed by NM, 8-May-1994.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ps  ->  B  =  C )   =>    |-  ( ( ps 
 /\  ph )  ->  A  =  C )
 
Theorem3eqtr3g 2143 A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)
 |-  ( ph  ->  A  =  B )   &    |-  A  =  C   &    |-  B  =  D   =>    |-  ( ph  ->  C  =  D )
 
Theorem3eqtr3a 2144 A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.)
 |-  A  =  B   &    |-  ( ph  ->  A  =  C )   &    |-  ( ph  ->  B  =  D )   =>    |-  ( ph  ->  C  =  D )
 
Theorem3eqtr4g 2145 A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-1993.)
 |-  ( ph  ->  A  =  B )   &    |-  C  =  A   &    |-  D  =  B   =>    |-  ( ph  ->  C  =  D )
 
Theorem3eqtr4a 2146 A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  A  =  B   &    |-  ( ph  ->  C  =  A )   &    |-  ( ph  ->  D  =  B )   =>    |-  ( ph  ->  C  =  D )
 
Theoremeq2tri 2147 A compound transitive inference for class equality. (Contributed by NM, 22-Jan-2004.)
 |-  ( A  =  C  ->  D  =  F )   &    |-  ( B  =  D  ->  C  =  G )   =>    |-  ( ( A  =  C  /\  B  =  F ) 
 <->  ( B  =  D  /\  A  =  G ) )
 
Theoremeleq1w 2148 Weaker version of eleq1 2150 (but more general than elequ1 1647) not depending on ax-ext 2070 nor df-cleq 2081. (Contributed by BJ, 24-Jun-2019.)
 |-  ( x  =  y 
 ->  ( x  e.  A  <->  y  e.  A ) )
 
Theoremeleq2w 2149 Weaker version of eleq2 2151 (but more general than elequ2 1648) not depending on ax-ext 2070 nor df-cleq 2081. (Contributed by BJ, 29-Sep-2019.)
 |-  ( x  =  y 
 ->  ( A  e.  x  <->  A  e.  y ) )
 
Theoremeleq1 2150 Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
 |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
 
Theoremeleq2 2151 Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
 |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
 
Theoremeleq12 2152 Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.)
 |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  e.  C 
 <->  B  e.  D ) )
 
Theoremeleq1i 2153 Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
 |-  A  =  B   =>    |-  ( A  e.  C 
 <->  B  e.  C )
 
Theoremeleq2i 2154 Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
 |-  A  =  B   =>    |-  ( C  e.  A 
 <->  C  e.  B )
 
Theoremeleq12i 2155 Inference from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
 |-  A  =  B   &    |-  C  =  D   =>    |-  ( A  e.  C  <->  B  e.  D )
 
Theoremeleq1d 2156 Deduction from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
 |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  ( A  e.  C  <->  B  e.  C ) )
 
Theoremeleq2d 2157 Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.)
 |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  ( C  e.  A  <->  C  e.  B ) )
 
Theoremeleq12d 2158 Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  C  =  D )   =>    |-  ( ph  ->  ( A  e.  C  <->  B  e.  D ) )
 
Theoremeleq1a 2159 A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)
 |-  ( A  e.  B  ->  ( C  =  A  ->  C  e.  B ) )
 
Theoremeqeltri 2160 Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
 |-  A  =  B   &    |-  B  e.  C   =>    |-  A  e.  C
 
Theoremeqeltrri 2161 Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
 |-  A  =  B   &    |-  A  e.  C   =>    |-  B  e.  C
 
Theoremeleqtri 2162 Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
 |-  A  e.  B   &    |-  B  =  C   =>    |-  A  e.  C
 
Theoremeleqtrri 2163 Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
 |-  A  e.  B   &    |-  C  =  B   =>    |-  A  e.  C
 
Theoremeqeltrd 2164 Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  B  e.  C )   =>    |-  ( ph  ->  A  e.  C )
 
Theoremeqeltrrd 2165 Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  A  e.  C )   =>    |-  ( ph  ->  B  e.  C )
 
Theoremeleqtrd 2166 Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
 |-  ( ph  ->  A  e.  B )   &    |-  ( ph  ->  B  =  C )   =>    |-  ( ph  ->  A  e.  C )
 
Theoremeleqtrrd 2167 Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)
 |-  ( ph  ->  A  e.  B )   &    |-  ( ph  ->  C  =  B )   =>    |-  ( ph  ->  A  e.  C )
 
Theorem3eltr3i 2168 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
 |-  A  e.  B   &    |-  A  =  C   &    |-  B  =  D   =>    |-  C  e.  D
 
Theorem3eltr4i 2169 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
 |-  A  e.  B   &    |-  C  =  A   &    |-  D  =  B   =>    |-  C  e.  D
 
Theorem3eltr3d 2170 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
 |-  ( ph  ->  A  e.  B )   &    |-  ( ph  ->  A  =  C )   &    |-  ( ph  ->  B  =  D )   =>    |-  ( ph  ->  C  e.  D )
 
Theorem3eltr4d 2171 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
 |-  ( ph  ->  A  e.  B )   &    |-  ( ph  ->  C  =  A )   &    |-  ( ph  ->  D  =  B )   =>    |-  ( ph  ->  C  e.  D )
 
Theorem3eltr3g 2172 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
 |-  ( ph  ->  A  e.  B )   &    |-  A  =  C   &    |-  B  =  D   =>    |-  ( ph  ->  C  e.  D )
 
Theorem3eltr4g 2173 Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
 |-  ( ph  ->  A  e.  B )   &    |-  C  =  A   &    |-  D  =  B   =>    |-  ( ph  ->  C  e.  D )
 
Theoremsyl5eqel 2174 B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
 |-  A  =  B   &    |-  ( ph  ->  B  e.  C )   =>    |-  ( ph  ->  A  e.  C )
 
Theoremsyl5eqelr 2175 B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
 |-  B  =  A   &    |-  ( ph  ->  B  e.  C )   =>    |-  ( ph  ->  A  e.  C )
 
Theoremsyl5eleq 2176 B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
 |-  A  e.  B   &    |-  ( ph  ->  B  =  C )   =>    |-  ( ph  ->  A  e.  C )
 
Theoremsyl5eleqr 2177 B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
 |-  A  e.  B   &    |-  ( ph  ->  C  =  B )   =>    |-  ( ph  ->  A  e.  C )
 
Theoremsyl6eqel 2178 A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
 |-  ( ph  ->  A  =  B )   &    |-  B  e.  C   =>    |-  ( ph  ->  A  e.  C )
 
Theoremsyl6eqelr 2179 A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
 |-  ( ph  ->  B  =  A )   &    |-  B  e.  C   =>    |-  ( ph  ->  A  e.  C )
 
Theoremsyl6eleq 2180 A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
 |-  ( ph  ->  A  e.  B )   &    |-  B  =  C   =>    |-  ( ph  ->  A  e.  C )
 
Theoremsyl6eleqr 2181 A membership and equality inference. (Contributed by NM, 24-Apr-2005.)
 |-  ( ph  ->  A  e.  B )   &    |-  C  =  B   =>    |-  ( ph  ->  A  e.  C )
 
Theoremeleq2s 2182 Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
 |-  ( A  e.  B  -> 
 ph )   &    |-  C  =  B   =>    |-  ( A  e.  C  ->  ph )
 
Theoremeqneltrd 2183 If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  -.  B  e.  C )   =>    |-  ( ph  ->  -.  A  e.  C )
 
Theoremeqneltrrd 2184 If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  -.  A  e.  C )   =>    |-  ( ph  ->  -.  B  e.  C )
 
Theoremneleqtrd 2185 If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  -.  C  e.  A )   &    |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  -.  C  e.  B )
 
Theoremneleqtrrd 2186 If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017.)
 |-  ( ph  ->  -.  C  e.  B )   &    |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  -.  C  e.  A )
 
Theoremcleqh 2187* Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqf 2252. (Contributed by NM, 5-Aug-1993.)
 |-  ( y  e.  A  ->  A. x  y  e.  A )   &    |-  ( y  e.  B  ->  A. x  y  e.  B )   =>    |-  ( A  =  B 
 <-> 
 A. x ( x  e.  A  <->  x  e.  B ) )
 
Theoremnelneq 2188 A way of showing two classes are not equal. (Contributed by NM, 1-Apr-1997.)
 |-  ( ( A  e.  C  /\  -.  B  e.  C )  ->  -.  A  =  B )
 
Theoremnelneq2 2189 A way of showing two classes are not equal. (Contributed by NM, 12-Jan-2002.)
 |-  ( ( A  e.  B  /\  -.  A  e.  C )  ->  -.  B  =  C )
 
Theoremeqsb3lem 2190* Lemma for eqsb3 2191. (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
 |-  ( [ x  /  y ] y  =  A  <->  x  =  A )
 
Theoremeqsb3 2191* Substitution applied to an atomic wff (class version of equsb3 1873). (Contributed by Rodolfo Medina, 28-Apr-2010.)
 |-  ( [ x  /  y ] y  =  A  <->  x  =  A )
 
Theoremclelsb3 2192* Substitution applied to an atomic wff (class version of elsb3 1900). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
 |-  ( [ x  /  y ] y  e.  A  <->  x  e.  A )
 
Theoremclelsb4 2193* Substitution applied to an atomic wff (class version of elsb4 1901). (Contributed by Jim Kingdon, 22-Nov-2018.)
 |-  ( [ x  /  y ] A  e.  y  <->  A  e.  x )
 
Theoremhbxfreq 2194 A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfrbi 1406 for equivalence version. (Contributed by NM, 21-Aug-2007.)
 |-  A  =  B   &    |-  (
 y  e.  B  ->  A. x  y  e.  B )   =>    |-  ( y  e.  A  ->  A. x  y  e.  A )
 
Theoremhblem 2195* Change the free variable of a hypothesis builder. (Contributed by NM, 5-Aug-1993.) (Revised by Andrew Salmon, 11-Jul-2011.)
 |-  ( y  e.  A  ->  A. x  y  e.  A )   =>    |-  ( z  e.  A  ->  A. x  z  e.  A )
 
Theoremabeq2 2196* Equality of a class variable and a class abstraction (also called a class builder). Theorem 5.1 of [Quine] p. 34. This theorem shows the relationship between expressions with class abstractions and expressions with class variables. Note that abbi 2201 and its relatives are among those useful for converting theorems with class variables to equivalent theorems with wff variables, by first substituting a class abstraction for each class variable.

Class variables can always be eliminated from a theorem to result in an equivalent theorem with wff variables, and vice-versa. The idea is roughly as follows. To convert a theorem with a wff variable  ph (that has a free variable  x) to a theorem with a class variable  A, we substitute  x  e.  A for  ph throughout and simplify, where  A is a new class variable not already in the wff. Conversely, to convert a theorem with a class variable  A to one with  ph, we substitute  { x  |  ph } for  A throughout and simplify, where  x and  ph are new set and wff variables not already in the wff. For more information on class variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13. (Contributed by NM, 5-Aug-1993.)

 |-  ( A  =  { x  |  ph }  <->  A. x ( x  e.  A  <->  ph ) )
 
Theoremabeq1 2197* Equality of a class variable and a class abstraction. (Contributed by NM, 20-Aug-1993.)
 |-  ( { x  |  ph
 }  =  A  <->  A. x ( ph  <->  x  e.  A ) )
 
Theoremabeq2i 2198 Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996.)
 |-  A  =  { x  |  ph }   =>    |-  ( x  e.  A  <->  ph )
 
Theoremabeq1i 2199 Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 31-Jul-1994.)
 |- 
 { x  |  ph }  =  A   =>    |-  ( ph  <->  x  e.  A )
 
Theoremabeq2d 2200 Equality of a class variable and a class abstraction (deduction). (Contributed by NM, 16-Nov-1995.)
 |-  ( ph  ->  A  =  { x  |  ps } )   =>    |-  ( ph  ->  ( x  e.  A  <->  ps ) )
    < Previous  Next >

Page List
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-11571
  Copyright terms: Public domain < Previous  Next >