MPE Home Metamath Proof Explorer This is the Unicode version.
Change to GIF version

List of Theorems
RefDescription
idi 1 (_Note_: This inference r...
a1ii 2 (_Note_: This inference r...
mp2 9 A double modus ponens infe...
mp2b 10 A double modus ponens infe...
a1i 11 Inference introducing an a...
2a1i 12 Inference introducing two ...
mp1i 13 Inference detaching an ant...
a2i 14 Inference distributing an ...
mpd 15 A modus ponens deduction. ...
imim2i 16 Inference adding common an...
syl 17 An inference version of th...
3syl 18 Inference chaining two syl...
4syl 19 Inference chaining three s...
mpi 20 A nested modus ponens infe...
mpisyl 21 A syllogism combined with ...
id 22 Principle of identity. Th...
idALT 23 Alternate proof of ~ id . ...
idd 24 Principle of identity ~ id...
a1d 25 Deduction introducing an e...
2a1d 26 Deduction introducing two ...
a1i13 27 Add two antecedents to a w...
2a1 28 A double form of ~ ax-1 . ...
a2d 29 Deduction distributing an ...
sylcom 30 Syllogism inference with c...
syl5com 31 Syllogism inference with c...
com12 32 Inference that swaps (comm...
syl11 33 A syllogism inference. Co...
syl5 34 A syllogism rule of infere...
syl6 35 A syllogism rule of infere...
syl56 36 Combine ~ syl5 and ~ syl6 ...
syl6com 37 Syllogism inference with c...
mpcom 38 Modus ponens inference wit...
syli 39 Syllogism inference with c...
syl2im 40 Replace two antecedents. ...
syl2imc 41 A commuted version of ~ sy...
pm2.27 42 This theorem, sometimes ca...
mpdd 43 A nested modus ponens dedu...
mpid 44 A nested modus ponens dedu...
mpdi 45 A nested modus ponens dedu...
mpii 46 A doubly nested modus pone...
syld 47 Syllogism deduction. Dedu...
syldc 48 Syllogism deduction. Comm...
mp2d 49 A double modus ponens dedu...
a1dd 50 Double deduction introduci...
2a1dd 51 Double deduction introduci...
pm2.43i 52 Inference absorbing redund...
pm2.43d 53 Deduction absorbing redund...
pm2.43a 54 Inference absorbing redund...
pm2.43b 55 Inference absorbing redund...
pm2.43 56 Absorption of redundant an...
imim2d 57 Deduction adding nested an...
imim2 58 A closed form of syllogism...
embantd 59 Deduction embedding an ant...
3syld 60 Triple syllogism deduction...
sylsyld 61 A double syllogism inferen...
imim12i 62 Inference joining two impl...
imim1i 63 Inference adding common co...
imim3i 64 Inference adding three nes...
sylc 65 A syllogism inference comb...
syl3c 66 A syllogism inference comb...
syl6mpi 67 A syllogism inference. (C...
mpsyl 68 Modus ponens combined with...
mpsylsyld 69 Modus ponens combined with...
syl6c 70 Inference combining ~ syl6...
syl6ci 71 A syllogism inference comb...
syldd 72 Nested syllogism deduction...
syl5d 73 A nested syllogism deducti...
syl7 74 A syllogism rule of infere...
syl6d 75 A nested syllogism deducti...
syl8 76 A syllogism rule of infere...
syl9 77 A nested syllogism inferen...
syl9r 78 A nested syllogism inferen...
syl10 79 A nested syllogism inferen...
a1ddd 80 Triple deduction introduci...
imim12d 81 Deduction combining antece...
imim1d 82 Deduction adding nested co...
imim1 83 A closed form of syllogism...
pm2.83 84 Theorem *2.83 of [Whitehea...
peirceroll 85 Over minimal implicational...
com23 86 Commutation of antecedents...
com3r 87 Commutation of antecedents...
com13 88 Commutation of antecedents...
com3l 89 Commutation of antecedents...
pm2.04 90 Swap antecedents. Theorem...
com34 91 Commutation of antecedents...
com4l 92 Commutation of antecedents...
com4t 93 Commutation of antecedents...
com4r 94 Commutation of antecedents...
com24 95 Commutation of antecedents...
com14 96 Commutation of antecedents...
com45 97 Commutation of antecedents...
com35 98 Commutation of antecedents...
com25 99 Commutation of antecedents...
com5l 100 Commutation of antecedents...
com15 101 Commutation of antecedents...
com52l 102 Commutation of antecedents...
com52r 103 Commutation of antecedents...
com5r 104 Commutation of antecedents...
imim12 105 Closed form of ~ imim12i a...
jarr 106 Elimination of a nested an...
jarri 107 Inference associated with ...
pm2.86d 108 Deduction associated with ...
pm2.86 109 Converse of Axiom ~ ax-2 ....
pm2.86i 110 Inference associated with ...
loolin 111 The Linearity Axiom of the...
loowoz 112 An alternate for the Linea...
con4 113 Alias for ~ ax-3 to be use...
con4i 114 Inference associated with ...
con4d 115 Deduction associated with ...
mt4 116 The rule of modus tollens....
mt4d 117 Modus tollens deduction. ...
mt4i 118 Modus tollens inference. ...
pm2.21i 119 A contradiction implies an...
pm2.24ii 120 A contradiction implies an...
pm2.21d 121 A contradiction implies an...
pm2.21ddALT 122 Alternate proof of ~ pm2.2...
pm2.21 123 From a wff and its negatio...
pm2.24 124 Theorem *2.24 of [Whitehea...
jarl 125 Elimination of a nested an...
jarli 126 Inference associated with ...
pm2.18d 127 Deduction form of the Clav...
pm2.18 128 Clavius law, or "consequen...
pm2.18OLD 129 Obsolete version of ~ pm2....
pm2.18dOLD 130 Obsolete version of ~ pm2....
pm2.18i 131 Inference associated with ...
notnotr 132 Double negation eliminatio...
notnotri 133 Inference associated with ...
notnotriALT 134 Alternate proof of ~ notno...
notnotrd 135 Deduction associated with ...
con2d 136 A contraposition deduction...
con2 137 Contraposition. Theorem *...
mt2d 138 Modus tollens deduction. ...
mt2i 139 Modus tollens inference. ...
nsyl3 140 A negated syllogism infere...
con2i 141 A contraposition inference...
nsyl 142 A negated syllogism infere...
nsyl2 143 A negated syllogism infere...
notnot 144 Double negation introducti...
notnoti 145 Inference associated with ...
notnotd 146 Deduction associated with ...
con1d 147 A contraposition deduction...
con1 148 Contraposition. Theorem *...
con1i 149 A contraposition inference...
mt3d 150 Modus tollens deduction. ...
mt3i 151 Modus tollens inference. ...
nsyl2OLD 152 Obsolete version of ~ nsyl...
pm2.24i 153 Inference associated with ...
pm2.24d 154 Deduction form of ~ pm2.24...
con3d 155 A contraposition deduction...
con3 156 Contraposition. Theorem *...
con3i 157 A contraposition inference...
con3rr3 158 Rotate through consequent ...
nsyld 159 A negated syllogism deduct...
nsyli 160 A negated syllogism infere...
nsyl4 161 A negated syllogism infere...
nsyl5 162 A negated syllogism infere...
pm3.2im 163 Theorem *3.2 of [Whitehead...
jc 164 Deduction joining the cons...
jcn 165 Theorem joining the conseq...
jcnd 166 Deduction joining the cons...
impi 167 An importation inference. ...
expi 168 An exportation inference. ...
simprim 169 Simplification. Similar t...
simplim 170 Simplification. Similar t...
pm2.5g 171 General instance of Theore...
pm2.5 172 Theorem *2.5 of [Whitehead...
conax1 173 Contrapositive of ~ ax-1 ....
conax1k 174 Weakening of ~ conax1 . G...
pm2.51 175 Theorem *2.51 of [Whitehea...
pm2.52 176 Theorem *2.52 of [Whitehea...
pm2.521g 177 A general instance of Theo...
pm2.521g2 178 A general instance of Theo...
pm2.521 179 Theorem *2.521 of [Whitehe...
expt 180 Exportation theorem ~ pm3....
impt 181 Importation theorem ~ pm3....
pm2.61d 182 Deduction eliminating an a...
pm2.61d1 183 Inference eliminating an a...
pm2.61d2 184 Inference eliminating an a...
pm2.61i 185 Inference eliminating an a...
pm2.61ii 186 Inference eliminating two ...
pm2.61nii 187 Inference eliminating two ...
pm2.61iii 188 Inference eliminating thre...
ja 189 Inference joining the ante...
jad 190 Deduction form of ~ ja . ...
pm2.61iOLD 191 Obsolete version of ~ pm2....
pm2.01 192 Weak Clavius law. If a fo...
pm2.01d 193 Deduction based on reducti...
pm2.6 194 Theorem *2.6 of [Whitehead...
pm2.61 195 Theorem *2.61 of [Whitehea...
pm2.65 196 Theorem *2.65 of [Whitehea...
pm2.65i 197 Inference for proof by con...
pm2.21dd 198 A contradiction implies an...
pm2.65d 199 Deduction for proof by con...
mto 200 The rule of modus tollens....
mtod 201 Modus tollens deduction. ...
mtoi 202 Modus tollens inference. ...
mt2 203 A rule similar to modus to...
mt3 204 A rule similar to modus to...
peirce 205 Peirce's axiom. A non-int...
looinv 206 The Inversion Axiom of the...
bijust0 207 A self-implication (see ~ ...
bijust 208 Theorem used to justify th...
impbi 211 Property of the biconditio...
impbii 212 Infer an equivalence from ...
impbidd 213 Deduce an equivalence from...
impbid21d 214 Deduce an equivalence from...
impbid 215 Deduce an equivalence from...
dfbi1 216 Relate the biconditional c...
dfbi1ALT 217 Alternate proof of ~ dfbi1...
biimp 218 Property of the biconditio...
biimpi 219 Infer an implication from ...
sylbi 220 A mixed syllogism inferenc...
sylib 221 A mixed syllogism inferenc...
sylbb 222 A mixed syllogism inferenc...
biimpr 223 Property of the biconditio...
bicom1 224 Commutative law for the bi...
bicom 225 Commutative law for the bi...
bicomd 226 Commute two sides of a bic...
bicomi 227 Inference from commutative...
impbid1 228 Infer an equivalence from ...
impbid2 229 Infer an equivalence from ...
impcon4bid 230 A variation on ~ impbid wi...
biimpri 231 Infer a converse implicati...
biimpd 232 Deduce an implication from...
mpbi 233 An inference from a bicond...
mpbir 234 An inference from a bicond...
mpbid 235 A deduction from a bicondi...
mpbii 236 An inference from a nested...
sylibr 237 A mixed syllogism inferenc...
sylbir 238 A mixed syllogism inferenc...
sylbbr 239 A mixed syllogism inferenc...
sylbb1 240 A mixed syllogism inferenc...
sylbb2 241 A mixed syllogism inferenc...
sylibd 242 A syllogism deduction. (C...
sylbid 243 A syllogism deduction. (C...
mpbidi 244 A deduction from a bicondi...
syl5bi 245 A mixed syllogism inferenc...
syl5bir 246 A mixed syllogism inferenc...
syl5ib 247 A mixed syllogism inferenc...
syl5ibcom 248 A mixed syllogism inferenc...
syl5ibr 249 A mixed syllogism inferenc...
syl5ibrcom 250 A mixed syllogism inferenc...
biimprd 251 Deduce a converse implicat...
biimpcd 252 Deduce a commuted implicat...
biimprcd 253 Deduce a converse commuted...
syl6ib 254 A mixed syllogism inferenc...
syl6ibr 255 A mixed syllogism inferenc...
syl6bi 256 A mixed syllogism inferenc...
syl6bir 257 A mixed syllogism inferenc...
syl7bi 258 A mixed syllogism inferenc...
syl8ib 259 A syllogism rule of infere...
mpbird 260 A deduction from a bicondi...
mpbiri 261 An inference from a nested...
sylibrd 262 A syllogism deduction. (C...
sylbird 263 A syllogism deduction. (C...
biid 264 Principle of identity for ...
biidd 265 Principle of identity with...
pm5.1im 266 Two propositions are equiv...
2th 267 Two truths are equivalent....
2thd 268 Two truths are equivalent....
monothetic 269 Two self-implications (see...
ibi 270 Inference that converts a ...
ibir 271 Inference that converts a ...
ibd 272 Deduction that converts a ...
pm5.74 273 Distribution of implicatio...
pm5.74i 274 Distribution of implicatio...
pm5.74ri 275 Distribution of implicatio...
pm5.74d 276 Distribution of implicatio...
pm5.74rd 277 Distribution of implicatio...
bitri 278 An inference from transiti...
bitr2i 279 An inference from transiti...
bitr3i 280 An inference from transiti...
bitr4i 281 An inference from transiti...
bitrd 282 Deduction form of ~ bitri ...
bitr2d 283 Deduction form of ~ bitr2i...
bitr3d 284 Deduction form of ~ bitr3i...
bitr4d 285 Deduction form of ~ bitr4i...
syl5bb 286 A syllogism inference from...
syl5rbb 287 A syllogism inference from...
bitr3id 288 A syllogism inference from...
bitr3di 289 A syllogism inference from...
bitrdi 290 A syllogism inference from...
bitr2di 291 A syllogism inference from...
bitr4di 292 A syllogism inference from...
bitr4id 293 A syllogism inference from...
3imtr3i 294 A mixed syllogism inferenc...
3imtr4i 295 A mixed syllogism inferenc...
3imtr3d 296 More general version of ~ ...
3imtr4d 297 More general version of ~ ...
3imtr3g 298 More general version of ~ ...
3imtr4g 299 More general version of ~ ...
3bitri 300 A chained inference from t...
3bitrri 301 A chained inference from t...
3bitr2i 302 A chained inference from t...
3bitr2ri 303 A chained inference from t...
3bitr3i 304 A chained inference from t...
3bitr3ri 305 A chained inference from t...
3bitr4i 306 A chained inference from t...
3bitr4ri 307 A chained inference from t...
3bitrd 308 Deduction from transitivit...
3bitrrd 309 Deduction from transitivit...
3bitr2d 310 Deduction from transitivit...
3bitr2rd 311 Deduction from transitivit...
3bitr3d 312 Deduction from transitivit...
3bitr3rd 313 Deduction from transitivit...
3bitr4d 314 Deduction from transitivit...
3bitr4rd 315 Deduction from transitivit...
3bitr3g 316 More general version of ~ ...
3bitr4g 317 More general version of ~ ...
notnotb 318 Double negation. Theorem ...
con34b 319 A biconditional form of co...
con4bid 320 A contraposition deduction...
notbid 321 Deduction negating both si...
notbi 322 Contraposition. Theorem *...
notbii 323 Negate both sides of a log...
con4bii 324 A contraposition inference...
mtbi 325 An inference from a bicond...
mtbir 326 An inference from a bicond...
mtbid 327 A deduction from a bicondi...
mtbird 328 A deduction from a bicondi...
mtbii 329 An inference from a bicond...
mtbiri 330 An inference from a bicond...
sylnib 331 A mixed syllogism inferenc...
sylnibr 332 A mixed syllogism inferenc...
sylnbi 333 A mixed syllogism inferenc...
sylnbir 334 A mixed syllogism inferenc...
xchnxbi 335 Replacement of a subexpres...
xchnxbir 336 Replacement of a subexpres...
xchbinx 337 Replacement of a subexpres...
xchbinxr 338 Replacement of a subexpres...
imbi2i 339 Introduce an antecedent to...
jcndOLD 340 Obsolete version of ~ jcnd...
bibi2i 341 Inference adding a bicondi...
bibi1i 342 Inference adding a bicondi...
bibi12i 343 The equivalence of two equ...
imbi2d 344 Deduction adding an antece...
imbi1d 345 Deduction adding a consequ...
bibi2d 346 Deduction adding a bicondi...
bibi1d 347 Deduction adding a bicondi...
imbi12d 348 Deduction joining two equi...
bibi12d 349 Deduction joining two equi...
imbi12 350 Closed form of ~ imbi12i ....
imbi1 351 Theorem *4.84 of [Whitehea...
imbi2 352 Theorem *4.85 of [Whitehea...
imbi1i 353 Introduce a consequent to ...
imbi12i 354 Join two logical equivalen...
bibi1 355 Theorem *4.86 of [Whitehea...
bitr3 356 Closed nested implication ...
con2bi 357 Contraposition. Theorem *...
con2bid 358 A contraposition deduction...
con1bid 359 A contraposition deduction...
con1bii 360 A contraposition inference...
con2bii 361 A contraposition inference...
con1b 362 Contraposition. Bidirecti...
con2b 363 Contraposition. Bidirecti...
biimt 364 A wff is equivalent to its...
pm5.5 365 Theorem *5.5 of [Whitehead...
a1bi 366 Inference introducing a th...
mt2bi 367 A false consequent falsifi...
mtt 368 Modus-tollens-like theorem...
imnot 369 If a proposition is false,...
pm5.501 370 Theorem *5.501 of [Whitehe...
ibib 371 Implication in terms of im...
ibibr 372 Implication in terms of im...
tbt 373 A wff is equivalent to its...
nbn2 374 The negation of a wff is e...
bibif 375 Transfer negation via an e...
nbn 376 The negation of a wff is e...
nbn3 377 Transfer falsehood via equ...
pm5.21im 378 Two propositions are equiv...
2false 379 Two falsehoods are equival...
2falsed 380 Two falsehoods are equival...
2falsedOLD 381 Obsolete version of ~ 2fal...
pm5.21ni 382 Two propositions implying ...
pm5.21nii 383 Eliminate an antecedent im...
pm5.21ndd 384 Eliminate an antecedent im...
bija 385 Combine antecedents into a...
pm5.18 386 Theorem *5.18 of [Whitehea...
xor3 387 Two ways to express "exclu...
nbbn 388 Move negation outside of b...
biass 389 Associative law for the bi...
biluk 390 Lukasiewicz's shortest axi...
pm5.19 391 Theorem *5.19 of [Whitehea...
bi2.04 392 Logical equivalence of com...
pm5.4 393 Antecedent absorption impl...
imdi 394 Distributive law for impli...
pm5.41 395 Theorem *5.41 of [Whitehea...
pm4.8 396 Theorem *4.8 of [Whitehead...
pm4.81 397 A formula is equivalent to...
imim21b 398 Simplify an implication be...
pm4.63 401 Theorem *4.63 of [Whitehea...
pm4.67 402 Theorem *4.67 of [Whitehea...
imnan 403 Express an implication in ...
imnani 404 Infer an implication from ...
iman 405 Implication in terms of co...
pm3.24 406 Law of noncontradiction. ...
annim 407 Express a conjunction in t...
pm4.61 408 Theorem *4.61 of [Whitehea...
pm4.65 409 Theorem *4.65 of [Whitehea...
imp 410 Importation inference. (C...
impcom 411 Importation inference with...
con3dimp 412 Variant of ~ con3d with im...
mpnanrd 413 Eliminate the right side o...
impd 414 Importation deduction. (C...
impcomd 415 Importation deduction with...
ex 416 Exportation inference. (T...
expcom 417 Exportation inference with...
expdcom 418 Commuted form of ~ expd . ...
expd 419 Exportation deduction. (C...
expcomd 420 Deduction form of ~ expcom...
imp31 421 An importation inference. ...
imp32 422 An importation inference. ...
exp31 423 An exportation inference. ...
exp32 424 An exportation inference. ...
imp4b 425 An importation inference. ...
imp4a 426 An importation inference. ...
imp4c 427 An importation inference. ...
imp4d 428 An importation inference. ...
imp41 429 An importation inference. ...
imp42 430 An importation inference. ...
imp43 431 An importation inference. ...
imp44 432 An importation inference. ...
imp45 433 An importation inference. ...
exp4b 434 An exportation inference. ...
exp4a 435 An exportation inference. ...
exp4c 436 An exportation inference. ...
exp4d 437 An exportation inference. ...
exp41 438 An exportation inference. ...
exp42 439 An exportation inference. ...
exp43 440 An exportation inference. ...
exp44 441 An exportation inference. ...
exp45 442 An exportation inference. ...
imp5d 443 An importation inference. ...
imp5a 444 An importation inference. ...
imp5g 445 An importation inference. ...
imp55 446 An importation inference. ...
imp511 447 An importation inference. ...
exp5c 448 An exportation inference. ...
exp5j 449 An exportation inference. ...
exp5l 450 An exportation inference. ...
exp53 451 An exportation inference. ...
pm3.3 452 Theorem *3.3 (Exp) of [Whi...
pm3.31 453 Theorem *3.31 (Imp) of [Wh...
impexp 454 Import-export theorem. Pa...
impancom 455 Mixed importation/commutat...
expdimp 456 A deduction version of exp...
expimpd 457 Exportation followed by a ...
impr 458 Import a wff into a right ...
impl 459 Export a wff from a left c...
expr 460 Export a wff from a right ...
expl 461 Export a wff from a left c...
ancoms 462 Inference commuting conjun...
pm3.22 463 Theorem *3.22 of [Whitehea...
ancom 464 Commutative law for conjun...
ancomd 465 Commutation of conjuncts i...
biancomi 466 Commuting conjunction in a...
biancomd 467 Commuting conjunction in a...
ancomst 468 Closed form of ~ ancoms . ...
ancomsd 469 Deduction commuting conjun...
anasss 470 Associative law for conjun...
anassrs 471 Associative law for conjun...
anass 472 Associative law for conjun...
pm3.2 473 Join antecedents with conj...
pm3.2i 474 Infer conjunction of premi...
pm3.21 475 Join antecedents with conj...
pm3.43i 476 Nested conjunction of ante...
pm3.43 477 Theorem *3.43 (Comp) of [W...
dfbi2 478 A theorem similar to the s...
dfbi 479 Definition ~ df-bi rewritt...
biimpa 480 Importation inference from...
biimpar 481 Importation inference from...
biimpac 482 Importation inference from...
biimparc 483 Importation inference from...
adantr 484 Inference adding a conjunc...
adantl 485 Inference adding a conjunc...
simpl 486 Elimination of a conjunct....
simpli 487 Inference eliminating a co...
simpr 488 Elimination of a conjunct....
simpri 489 Inference eliminating a co...
intnan 490 Introduction of conjunct i...
intnanr 491 Introduction of conjunct i...
intnand 492 Introduction of conjunct i...
intnanrd 493 Introduction of conjunct i...
adantld 494 Deduction adding a conjunc...
adantrd 495 Deduction adding a conjunc...
pm3.41 496 Theorem *3.41 of [Whitehea...
pm3.42 497 Theorem *3.42 of [Whitehea...
simpld 498 Deduction eliminating a co...
simprd 499 Deduction eliminating a co...
simprbi 500 Deduction eliminating a co...
simplbi 501 Deduction eliminating a co...
simprbda 502 Deduction eliminating a co...
simplbda 503 Deduction eliminating a co...
simplbi2 504 Deduction eliminating a co...
simplbi2comt 505 Closed form of ~ simplbi2c...
simplbi2com 506 A deduction eliminating a ...
simpl2im 507 Implication from an elimin...
simplbiim 508 Implication from an elimin...
impel 509 An inference for implicati...
mpan9 510 Modus ponens conjoining di...
sylan9 511 Nested syllogism inference...
sylan9r 512 Nested syllogism inference...
sylan9bb 513 Nested syllogism inference...
sylan9bbr 514 Nested syllogism inference...
jca 515 Deduce conjunction of the ...
jcad 516 Deduction conjoining the c...
jca2 517 Inference conjoining the c...
jca31 518 Join three consequents. (...
jca32 519 Join three consequents. (...
jcai 520 Deduction replacing implic...
jcab 521 Distributive law for impli...
pm4.76 522 Theorem *4.76 of [Whitehea...
jctil 523 Inference conjoining a the...
jctir 524 Inference conjoining a the...
jccir 525 Inference conjoining a con...
jccil 526 Inference conjoining a con...
jctl 527 Inference conjoining a the...
jctr 528 Inference conjoining a the...
jctild 529 Deduction conjoining a the...
jctird 530 Deduction conjoining a the...
iba 531 Introduction of antecedent...
ibar 532 Introduction of antecedent...
biantru 533 A wff is equivalent to its...
biantrur 534 A wff is equivalent to its...
biantrud 535 A wff is equivalent to its...
biantrurd 536 A wff is equivalent to its...
bianfi 537 A wff conjoined with false...
bianfd 538 A wff conjoined with false...
baib 539 Move conjunction outside o...
baibr 540 Move conjunction outside o...
rbaibr 541 Move conjunction outside o...
rbaib 542 Move conjunction outside o...
baibd 543 Move conjunction outside o...
rbaibd 544 Move conjunction outside o...
bianabs 545 Absorb a hypothesis into t...
pm5.44 546 Theorem *5.44 of [Whitehea...
pm5.42 547 Theorem *5.42 of [Whitehea...
ancl 548 Conjoin antecedent to left...
anclb 549 Conjoin antecedent to left...
ancr 550 Conjoin antecedent to righ...
ancrb 551 Conjoin antecedent to righ...
ancli 552 Deduction conjoining antec...
ancri 553 Deduction conjoining antec...
ancld 554 Deduction conjoining antec...
ancrd 555 Deduction conjoining antec...
impac 556 Importation with conjuncti...
anc2l 557 Conjoin antecedent to left...
anc2r 558 Conjoin antecedent to righ...
anc2li 559 Deduction conjoining antec...
anc2ri 560 Deduction conjoining antec...
pm4.71 561 Implication in terms of bi...
pm4.71r 562 Implication in terms of bi...
pm4.71i 563 Inference converting an im...
pm4.71ri 564 Inference converting an im...
pm4.71d 565 Deduction converting an im...
pm4.71rd 566 Deduction converting an im...
pm4.24 567 Theorem *4.24 of [Whitehea...
anidm 568 Idempotent law for conjunc...
anidmdbi 569 Conjunction idempotence wi...
anidms 570 Inference from idempotent ...
imdistan 571 Distribution of implicatio...
imdistani 572 Distribution of implicatio...
imdistanri 573 Distribution of implicatio...
imdistand 574 Distribution of implicatio...
imdistanda 575 Distribution of implicatio...
pm5.3 576 Theorem *5.3 of [Whitehead...
pm5.32 577 Distribution of implicatio...
pm5.32i 578 Distribution of implicatio...
pm5.32ri 579 Distribution of implicatio...
pm5.32d 580 Distribution of implicatio...
pm5.32rd 581 Distribution of implicatio...
pm5.32da 582 Distribution of implicatio...
sylan 583 A syllogism inference. (C...
sylanb 584 A syllogism inference. (C...
sylanbr 585 A syllogism inference. (C...
sylanbrc 586 Syllogism inference. (Con...
syl2anc 587 Syllogism inference combin...
syl2anc2 588 Double syllogism inference...
sylancl 589 Syllogism inference combin...
sylancr 590 Syllogism inference combin...
sylancom 591 Syllogism inference with c...
sylanblc 592 Syllogism inference combin...
sylanblrc 593 Syllogism inference combin...
syldan 594 A syllogism deduction with...
sylbida 595 A syllogism deduction. (C...
sylan2 596 A syllogism inference. (C...
sylan2b 597 A syllogism inference. (C...
sylan2br 598 A syllogism inference. (C...
syl2an 599 A double syllogism inferen...
syl2anr 600 A double syllogism inferen...
syl2anb 601 A double syllogism inferen...
syl2anbr 602 A double syllogism inferen...
sylancb 603 A syllogism inference comb...
sylancbr 604 A syllogism inference comb...
syldanl 605 A syllogism deduction with...
syland 606 A syllogism deduction. (C...
sylani 607 A syllogism inference. (C...
sylan2d 608 A syllogism deduction. (C...
sylan2i 609 A syllogism inference. (C...
syl2ani 610 A syllogism inference. (C...
syl2and 611 A syllogism deduction. (C...
anim12d 612 Conjoin antecedents and co...
anim12d1 613 Variant of ~ anim12d where...
anim1d 614 Add a conjunct to right of...
anim2d 615 Add a conjunct to left of ...
anim12i 616 Conjoin antecedents and co...
anim12ci 617 Variant of ~ anim12i with ...
anim1i 618 Introduce conjunct to both...
anim1ci 619 Introduce conjunct to both...
anim2i 620 Introduce conjunct to both...
anim12ii 621 Conjoin antecedents and co...
anim12dan 622 Conjoin antecedents and co...
im2anan9 623 Deduction joining nested i...
im2anan9r 624 Deduction joining nested i...
pm3.45 625 Theorem *3.45 (Fact) of [W...
anbi2i 626 Introduce a left conjunct ...
anbi1i 627 Introduce a right conjunct...
anbi2ci 628 Variant of ~ anbi2i with c...
anbi1ci 629 Variant of ~ anbi1i with c...
anbi12i 630 Conjoin both sides of two ...
anbi12ci 631 Variant of ~ anbi12i with ...
anbi2d 632 Deduction adding a left co...
anbi1d 633 Deduction adding a right c...
anbi12d 634 Deduction joining two equi...
anbi1 635 Introduce a right conjunct...
anbi2 636 Introduce a left conjunct ...
anbi1cd 637 Introduce a proposition as...
pm4.38 638 Theorem *4.38 of [Whitehea...
bi2anan9 639 Deduction joining two equi...
bi2anan9r 640 Deduction joining two equi...
bi2bian9 641 Deduction joining two bico...
bianass 642 An inference to merge two ...
bianassc 643 An inference to merge two ...
an21 644 Swap two conjuncts. (Cont...
an12 645 Swap two conjuncts. Note ...
an32 646 A rearrangement of conjunc...
an13 647 A rearrangement of conjunc...
an31 648 A rearrangement of conjunc...
an12s 649 Swap two conjuncts in ante...
ancom2s 650 Inference commuting a nest...
an13s 651 Swap two conjuncts in ante...
an32s 652 Swap two conjuncts in ante...
ancom1s 653 Inference commuting a nest...
an31s 654 Swap two conjuncts in ante...
anass1rs 655 Commutative-associative la...
an4 656 Rearrangement of 4 conjunc...
an42 657 Rearrangement of 4 conjunc...
an43 658 Rearrangement of 4 conjunc...
an3 659 A rearrangement of conjunc...
an4s 660 Inference rearranging 4 co...
an42s 661 Inference rearranging 4 co...
anabs1 662 Absorption into embedded c...
anabs5 663 Absorption into embedded c...
anabs7 664 Absorption into embedded c...
anabsan 665 Absorption of antecedent w...
anabss1 666 Absorption of antecedent i...
anabss4 667 Absorption of antecedent i...
anabss5 668 Absorption of antecedent i...
anabsi5 669 Absorption of antecedent i...
anabsi6 670 Absorption of antecedent i...
anabsi7 671 Absorption of antecedent i...
anabsi8 672 Absorption of antecedent i...
anabss7 673 Absorption of antecedent i...
anabsan2 674 Absorption of antecedent w...
anabss3 675 Absorption of antecedent i...
anandi 676 Distribution of conjunctio...
anandir 677 Distribution of conjunctio...
anandis 678 Inference that undistribut...
anandirs 679 Inference that undistribut...
sylanl1 680 A syllogism inference. (C...
sylanl2 681 A syllogism inference. (C...
sylanr1 682 A syllogism inference. (C...
sylanr2 683 A syllogism inference. (C...
syl6an 684 A syllogism deduction comb...
syl2an2r 685 ~ syl2anr with antecedents...
syl2an2 686 ~ syl2an with antecedents ...
mpdan 687 An inference based on modu...
mpancom 688 An inference based on modu...
mpidan 689 A deduction which "stacks"...
mpan 690 An inference based on modu...
mpan2 691 An inference based on modu...
mp2an 692 An inference based on modu...
mp4an 693 An inference based on modu...
mpan2d 694 A deduction based on modus...
mpand 695 A deduction based on modus...
mpani 696 An inference based on modu...
mpan2i 697 An inference based on modu...
mp2ani 698 An inference based on modu...
mp2and 699 A deduction based on modus...
mpanl1 700 An inference based on modu...
mpanl2 701 An inference based on modu...
mpanl12 702 An inference based on modu...
mpanr1 703 An inference based on modu...
mpanr2 704 An inference based on modu...
mpanr12 705 An inference based on modu...
mpanlr1 706 An inference based on modu...
mpbirand 707 Detach truth from conjunct...
mpbiran2d 708 Detach truth from conjunct...
mpbiran 709 Detach truth from conjunct...
mpbiran2 710 Detach truth from conjunct...
mpbir2an 711 Detach a conjunction of tr...
mpbi2and 712 Detach a conjunction of tr...
mpbir2and 713 Detach a conjunction of tr...
adantll 714 Deduction adding a conjunc...
adantlr 715 Deduction adding a conjunc...
adantrl 716 Deduction adding a conjunc...
adantrr 717 Deduction adding a conjunc...
adantlll 718 Deduction adding a conjunc...
adantllr 719 Deduction adding a conjunc...
adantlrl 720 Deduction adding a conjunc...
adantlrr 721 Deduction adding a conjunc...
adantrll 722 Deduction adding a conjunc...
adantrlr 723 Deduction adding a conjunc...
adantrrl 724 Deduction adding a conjunc...
adantrrr 725 Deduction adding a conjunc...
ad2antrr 726 Deduction adding two conju...
ad2antlr 727 Deduction adding two conju...
ad2antrl 728 Deduction adding two conju...
ad2antll 729 Deduction adding conjuncts...
ad3antrrr 730 Deduction adding three con...
ad3antlr 731 Deduction adding three con...
ad4antr 732 Deduction adding 4 conjunc...
ad4antlr 733 Deduction adding 4 conjunc...
ad5antr 734 Deduction adding 5 conjunc...
ad5antlr 735 Deduction adding 5 conjunc...
ad6antr 736 Deduction adding 6 conjunc...
ad6antlr 737 Deduction adding 6 conjunc...
ad7antr 738 Deduction adding 7 conjunc...
ad7antlr 739 Deduction adding 7 conjunc...
ad8antr 740 Deduction adding 8 conjunc...
ad8antlr 741 Deduction adding 8 conjunc...
ad9antr 742 Deduction adding 9 conjunc...
ad9antlr 743 Deduction adding 9 conjunc...
ad10antr 744 Deduction adding 10 conjun...
ad10antlr 745 Deduction adding 10 conjun...
ad2ant2l 746 Deduction adding two conju...
ad2ant2r 747 Deduction adding two conju...
ad2ant2lr 748 Deduction adding two conju...
ad2ant2rl 749 Deduction adding two conju...
adantl3r 750 Deduction adding 1 conjunc...
ad4ant13 751 Deduction adding conjuncts...
ad4ant14 752 Deduction adding conjuncts...
ad4ant23 753 Deduction adding conjuncts...
ad4ant24 754 Deduction adding conjuncts...
adantl4r 755 Deduction adding 1 conjunc...
ad5ant12 756 Deduction adding conjuncts...
ad5ant13 757 Deduction adding conjuncts...
ad5ant14 758 Deduction adding conjuncts...
ad5ant15 759 Deduction adding conjuncts...
ad5ant23 760 Deduction adding conjuncts...
ad5ant24 761 Deduction adding conjuncts...
ad5ant25 762 Deduction adding conjuncts...
adantl5r 763 Deduction adding 1 conjunc...
adantl6r 764 Deduction adding 1 conjunc...
pm3.33 765 Theorem *3.33 (Syll) of [W...
pm3.34 766 Theorem *3.34 (Syll) of [W...
simpll 767 Simplification of a conjun...
simplld 768 Deduction form of ~ simpll...
simplr 769 Simplification of a conjun...
simplrd 770 Deduction eliminating a do...
simprl 771 Simplification of a conjun...
simprld 772 Deduction eliminating a do...
simprr 773 Simplification of a conjun...
simprrd 774 Deduction form of ~ simprr...
simplll 775 Simplification of a conjun...
simpllr 776 Simplification of a conjun...
simplrl 777 Simplification of a conjun...
simplrr 778 Simplification of a conjun...
simprll 779 Simplification of a conjun...
simprlr 780 Simplification of a conjun...
simprrl 781 Simplification of a conjun...
simprrr 782 Simplification of a conjun...
simp-4l 783 Simplification of a conjun...
simp-4r 784 Simplification of a conjun...
simp-5l 785 Simplification of a conjun...
simp-5r 786 Simplification of a conjun...
simp-6l 787 Simplification of a conjun...
simp-6r 788 Simplification of a conjun...
simp-7l 789 Simplification of a conjun...
simp-7r 790 Simplification of a conjun...
simp-8l 791 Simplification of a conjun...
simp-8r 792 Simplification of a conjun...
simp-9l 793 Simplification of a conjun...
simp-9r 794 Simplification of a conjun...
simp-10l 795 Simplification of a conjun...
simp-10r 796 Simplification of a conjun...
simp-11l 797 Simplification of a conjun...
simp-11r 798 Simplification of a conjun...
pm2.01da 799 Deduction based on reducti...
pm2.18da 800 Deduction based on reducti...
impbida 801 Deduce an equivalence from...
pm5.21nd 802 Eliminate an antecedent im...
pm3.35 803 Conjunctive detachment. T...
pm5.74da 804 Distribution of implicatio...
bitr 805 Theorem *4.22 of [Whitehea...
biantr 806 A transitive law of equiva...
pm4.14 807 Theorem *4.14 of [Whitehea...
pm3.37 808 Theorem *3.37 (Transp) of ...
anim12 809 Conjoin antecedents and co...
pm3.4 810 Conjunction implies implic...
exbiri 811 Inference form of ~ exbir ...
pm2.61ian 812 Elimination of an antecede...
pm2.61dan 813 Elimination of an antecede...
pm2.61ddan 814 Elimination of two anteced...
pm2.61dda 815 Elimination of two anteced...
mtand 816 A modus tollens deduction....
pm2.65da 817 Deduction for proof by con...
condan 818 Proof by contradiction. (...
biadan 819 An implication is equivale...
biadani 820 Inference associated with ...
biadaniALT 821 Alternate proof of ~ biada...
biadanii 822 Inference associated with ...
pm5.1 823 Two propositions are equiv...
pm5.21 824 Two propositions are equiv...
pm5.35 825 Theorem *5.35 of [Whitehea...
abai 826 Introduce one conjunct as ...
pm4.45im 827 Conjunction with implicati...
impimprbi 828 An implication and its rev...
nan 829 Theorem to move a conjunct...
pm5.31 830 Theorem *5.31 of [Whitehea...
pm5.31r 831 Variant of ~ pm5.31 . (Co...
pm4.15 832 Theorem *4.15 of [Whitehea...
pm5.36 833 Theorem *5.36 of [Whitehea...
annotanannot 834 A conjunction with a negat...
pm5.33 835 Theorem *5.33 of [Whitehea...
syl12anc 836 Syllogism combined with co...
syl21anc 837 Syllogism combined with co...
syl22anc 838 Syllogism combined with co...
syl1111anc 839 Four-hypothesis eliminatio...
syldbl2 840 Stacked hypotheseis implie...
mpsyl4anc 841 An elimination deduction. ...
pm4.87 842 Theorem *4.87 of [Whitehea...
bimsc1 843 Removal of conjunct from o...
a2and 844 Deduction distributing a c...
animpimp2impd 845 Deduction deriving nested ...
pm4.64 848 Theorem *4.64 of [Whitehea...
pm4.66 849 Theorem *4.66 of [Whitehea...
pm2.53 850 Theorem *2.53 of [Whitehea...
pm2.54 851 Theorem *2.54 of [Whitehea...
imor 852 Implication in terms of di...
imori 853 Infer disjunction from imp...
imorri 854 Infer implication from dis...
pm4.62 855 Theorem *4.62 of [Whitehea...
jaoi 856 Inference disjoining the a...
jao1i 857 Add a disjunct in the ante...
jaod 858 Deduction disjoining the a...
mpjaod 859 Eliminate a disjunction in...
ori 860 Infer implication from dis...
orri 861 Infer disjunction from imp...
orrd 862 Deduce disjunction from im...
ord 863 Deduce implication from di...
orci 864 Deduction introducing a di...
olci 865 Deduction introducing a di...
orc 866 Introduction of a disjunct...
olc 867 Introduction of a disjunct...
pm1.4 868 Axiom *1.4 of [WhiteheadRu...
orcom 869 Commutative law for disjun...
orcomd 870 Commutation of disjuncts i...
orcoms 871 Commutation of disjuncts i...
orcd 872 Deduction introducing a di...
olcd 873 Deduction introducing a di...
orcs 874 Deduction eliminating disj...
olcs 875 Deduction eliminating disj...
olcnd 876 A lemma for Conjunctive No...
unitreslOLD 877 Obsolete version of ~ olcn...
orcnd 878 A lemma for Conjunctive No...
mtord 879 A modus tollens deduction ...
pm3.2ni 880 Infer negated disjunction ...
pm2.45 881 Theorem *2.45 of [Whitehea...
pm2.46 882 Theorem *2.46 of [Whitehea...
pm2.47 883 Theorem *2.47 of [Whitehea...
pm2.48 884 Theorem *2.48 of [Whitehea...
pm2.49 885 Theorem *2.49 of [Whitehea...
norbi 886 If neither of two proposit...
nbior 887 If two propositions are no...
orel1 888 Elimination of disjunction...
pm2.25 889 Theorem *2.25 of [Whitehea...
orel2 890 Elimination of disjunction...
pm2.67-2 891 Slight generalization of T...
pm2.67 892 Theorem *2.67 of [Whitehea...
curryax 893 A non-intuitionistic posit...
exmid 894 Law of excluded middle, al...
exmidd 895 Law of excluded middle in ...
pm2.1 896 Theorem *2.1 of [Whitehead...
pm2.13 897 Theorem *2.13 of [Whitehea...
pm2.621 898 Theorem *2.621 of [Whitehe...
pm2.62 899 Theorem *2.62 of [Whitehea...
pm2.68 900 Theorem *2.68 of [Whitehea...
dfor2 901 Logical 'or' expressed in ...
pm2.07 902 Theorem *2.07 of [Whitehea...
pm1.2 903 Axiom *1.2 of [WhiteheadRu...
oridm 904 Idempotent law for disjunc...
pm4.25 905 Theorem *4.25 of [Whitehea...
pm2.4 906 Theorem *2.4 of [Whitehead...
pm2.41 907 Theorem *2.41 of [Whitehea...
orim12i 908 Disjoin antecedents and co...
orim1i 909 Introduce disjunct to both...
orim2i 910 Introduce disjunct to both...
orim12dALT 911 Alternate proof of ~ orim1...
orbi2i 912 Inference adding a left di...
orbi1i 913 Inference adding a right d...
orbi12i 914 Infer the disjunction of t...
orbi2d 915 Deduction adding a left di...
orbi1d 916 Deduction adding a right d...
orbi1 917 Theorem *4.37 of [Whitehea...
orbi12d 918 Deduction joining two equi...
pm1.5 919 Axiom *1.5 (Assoc) of [Whi...
or12 920 Swap two disjuncts. (Cont...
orass 921 Associative law for disjun...
pm2.31 922 Theorem *2.31 of [Whitehea...
pm2.32 923 Theorem *2.32 of [Whitehea...
pm2.3 924 Theorem *2.3 of [Whitehead...
or32 925 A rearrangement of disjunc...
or4 926 Rearrangement of 4 disjunc...
or42 927 Rearrangement of 4 disjunc...
orordi 928 Distribution of disjunctio...
orordir 929 Distribution of disjunctio...
orimdi 930 Disjunction distributes ov...
pm2.76 931 Theorem *2.76 of [Whitehea...
pm2.85 932 Theorem *2.85 of [Whitehea...
pm2.75 933 Theorem *2.75 of [Whitehea...
pm4.78 934 Implication distributes ov...
biort 935 A disjunction with a true ...
biorf 936 A wff is equivalent to its...
biortn 937 A wff is equivalent to its...
biorfi 938 A wff is equivalent to its...
pm2.26 939 Theorem *2.26 of [Whitehea...
pm2.63 940 Theorem *2.63 of [Whitehea...
pm2.64 941 Theorem *2.64 of [Whitehea...
pm2.42 942 Theorem *2.42 of [Whitehea...
pm5.11g 943 A general instance of Theo...
pm5.11 944 Theorem *5.11 of [Whitehea...
pm5.12 945 Theorem *5.12 of [Whitehea...
pm5.14 946 Theorem *5.14 of [Whitehea...
pm5.13 947 Theorem *5.13 of [Whitehea...
pm5.55 948 Theorem *5.55 of [Whitehea...
pm4.72 949 Implication in terms of bi...
imimorb 950 Simplify an implication be...
oibabs 951 Absorption of disjunction ...
orbidi 952 Disjunction distributes ov...
pm5.7 953 Disjunction distributes ov...
jaao 954 Inference conjoining and d...
jaoa 955 Inference disjoining and c...
jaoian 956 Inference disjoining the a...
jaodan 957 Deduction disjoining the a...
mpjaodan 958 Eliminate a disjunction in...
pm3.44 959 Theorem *3.44 of [Whitehea...
jao 960 Disjunction of antecedents...
jaob 961 Disjunction of antecedents...
pm4.77 962 Theorem *4.77 of [Whitehea...
pm3.48 963 Theorem *3.48 of [Whitehea...
orim12d 964 Disjoin antecedents and co...
orim1d 965 Disjoin antecedents and co...
orim2d 966 Disjoin antecedents and co...
orim2 967 Axiom *1.6 (Sum) of [White...
pm2.38 968 Theorem *2.38 of [Whitehea...
pm2.36 969 Theorem *2.36 of [Whitehea...
pm2.37 970 Theorem *2.37 of [Whitehea...
pm2.81 971 Theorem *2.81 of [Whitehea...
pm2.8 972 Theorem *2.8 of [Whitehead...
pm2.73 973 Theorem *2.73 of [Whitehea...
pm2.74 974 Theorem *2.74 of [Whitehea...
pm2.82 975 Theorem *2.82 of [Whitehea...
pm4.39 976 Theorem *4.39 of [Whitehea...
animorl 977 Conjunction implies disjun...
animorr 978 Conjunction implies disjun...
animorlr 979 Conjunction implies disjun...
animorrl 980 Conjunction implies disjun...
ianor 981 Negated conjunction in ter...
anor 982 Conjunction in terms of di...
ioran 983 Negated disjunction in ter...
pm4.52 984 Theorem *4.52 of [Whitehea...
pm4.53 985 Theorem *4.53 of [Whitehea...
pm4.54 986 Theorem *4.54 of [Whitehea...
pm4.55 987 Theorem *4.55 of [Whitehea...
pm4.56 988 Theorem *4.56 of [Whitehea...
oran 989 Disjunction in terms of co...
pm4.57 990 Theorem *4.57 of [Whitehea...
pm3.1 991 Theorem *3.1 of [Whitehead...
pm3.11 992 Theorem *3.11 of [Whitehea...
pm3.12 993 Theorem *3.12 of [Whitehea...
pm3.13 994 Theorem *3.13 of [Whitehea...
pm3.14 995 Theorem *3.14 of [Whitehea...
pm4.44 996 Theorem *4.44 of [Whitehea...
pm4.45 997 Theorem *4.45 of [Whitehea...
orabs 998 Absorption of redundant in...
oranabs 999 Absorb a disjunct into a c...
pm5.61 1000 Theorem *5.61 of [Whitehea...
pm5.6 1001 Conjunction in antecedent ...
orcanai 1002 Change disjunction in cons...
pm4.79 1003 Theorem *4.79 of [Whitehea...
pm5.53 1004 Theorem *5.53 of [Whitehea...
ordi 1005 Distributive law for disju...
ordir 1006 Distributive law for disju...
andi 1007 Distributive law for conju...
andir 1008 Distributive law for conju...
orddi 1009 Double distributive law fo...
anddi 1010 Double distributive law fo...
pm5.17 1011 Theorem *5.17 of [Whitehea...
pm5.15 1012 Theorem *5.15 of [Whitehea...
pm5.16 1013 Theorem *5.16 of [Whitehea...
xor 1014 Two ways to express exclus...
nbi2 1015 Two ways to express "exclu...
xordi 1016 Conjunction distributes ov...
pm5.54 1017 Theorem *5.54 of [Whitehea...
pm5.62 1018 Theorem *5.62 of [Whitehea...
pm5.63 1019 Theorem *5.63 of [Whitehea...
niabn 1020 Miscellaneous inference re...
ninba 1021 Miscellaneous inference re...
pm4.43 1022 Theorem *4.43 of [Whitehea...
pm4.82 1023 Theorem *4.82 of [Whitehea...
pm4.83 1024 Theorem *4.83 of [Whitehea...
pclem6 1025 Negation inferred from emb...
bigolden 1026 Dijkstra-Scholten's Golden...
pm5.71 1027 Theorem *5.71 of [Whitehea...
pm5.75 1028 Theorem *5.75 of [Whitehea...
ecase2d 1029 Deduction for elimination ...
ecase2dOLD 1030 Obsolete version of ~ ecas...
ecase3 1031 Inference for elimination ...
ecase 1032 Inference for elimination ...
ecase3d 1033 Deduction for elimination ...
ecased 1034 Deduction for elimination ...
ecase3ad 1035 Deduction for elimination ...
ecase3adOLD 1036 Obsolete version of ~ ecas...
ccase 1037 Inference for combining ca...
ccased 1038 Deduction for combining ca...
ccase2 1039 Inference for combining ca...
4cases 1040 Inference eliminating two ...
4casesdan 1041 Deduction eliminating two ...
cases 1042 Case disjunction according...
dedlem0a 1043 Lemma for an alternate ver...
dedlem0b 1044 Lemma for an alternate ver...
dedlema 1045 Lemma for weak deduction t...
dedlemb 1046 Lemma for weak deduction t...
cases2 1047 Case disjunction according...
cases2ALT 1048 Alternate proof of ~ cases...
dfbi3 1049 An alternate definition of...
pm5.24 1050 Theorem *5.24 of [Whitehea...
4exmid 1051 The disjunction of the fou...
consensus 1052 The consensus theorem. Th...
pm4.42 1053 Theorem *4.42 of [Whitehea...
prlem1 1054 A specialized lemma for se...
prlem2 1055 A specialized lemma for se...
oplem1 1056 A specialized lemma for se...
dn1 1057 A single axiom for Boolean...
bianir 1058 A closed form of ~ mpbir ,...
jaoi2 1059 Inference removing a negat...
jaoi3 1060 Inference separating a dis...
ornld 1061 Selecting one statement fr...
dfifp2 1064 Alternate definition of th...
dfifp3 1065 Alternate definition of th...
dfifp4 1066 Alternate definition of th...
dfifp5 1067 Alternate definition of th...
dfifp6 1068 Alternate definition of th...
dfifp7 1069 Alternate definition of th...
ifpdfbi 1070 Define the biconditional a...
anifp 1071 The conditional operator i...
ifpor 1072 The conditional operator i...
ifpn 1073 Conditional operator for t...
ifpnOLD 1074 Obsolete version of ~ ifpn...
ifptru 1075 Value of the conditional o...
ifpfal 1076 Value of the conditional o...
ifpid 1077 Value of the conditional o...
casesifp 1078 Version of ~ cases express...
ifpbi123d 1079 Equivalence deduction for ...
ifpbi123dOLD 1080 Obsolete version of ~ ifpb...
ifpbi23d 1081 Equivalence deduction for ...
ifpimpda 1082 Separation of the values o...
1fpid3 1083 The value of the condition...
elimh 1084 Hypothesis builder for the...
dedt 1085 The weak deduction theorem...
con3ALT 1086 Proof of ~ con3 from its a...
3orass 1091 Associative law for triple...
3orel1 1092 Partial elimination of a t...
3orrot 1093 Rotation law for triple di...
3orcoma 1094 Commutation law for triple...
3orcomb 1095 Commutation law for triple...
3anass 1096 Associative law for triple...
3anan12 1097 Convert triple conjunction...
3anan32 1098 Convert triple conjunction...
3ancoma 1099 Commutation law for triple...
3ancomb 1100 Commutation law for triple...
3anrot 1101 Rotation law for triple co...
3anrev 1102 Reversal law for triple co...
anandi3 1103 Distribution of triple con...
anandi3r 1104 Distribution of triple con...
3anidm 1105 Idempotent law for conjunc...
3an4anass 1106 Associative law for four c...
3ioran 1107 Negated triple disjunction...
3ianor 1108 Negated triple conjunction...
3anor 1109 Triple conjunction express...
3oran 1110 Triple disjunction in term...
3impa 1111 Importation from double to...
3imp 1112 Importation inference. (C...
3imp31 1113 The importation inference ...
3imp231 1114 Importation inference. (C...
3imp21 1115 The importation inference ...
3impb 1116 Importation from double to...
3impib 1117 Importation to triple conj...
3impia 1118 Importation to triple conj...
3expa 1119 Exportation from triple to...
3exp 1120 Exportation inference. (C...
3expb 1121 Exportation from triple to...
3expia 1122 Exportation from triple co...
3expib 1123 Exportation from triple co...
3com12 1124 Commutation in antecedent....
3com13 1125 Commutation in antecedent....
3comr 1126 Commutation in antecedent....
3com23 1127 Commutation in antecedent....
3coml 1128 Commutation in antecedent....
3jca 1129 Join consequents with conj...
3jcad 1130 Deduction conjoining the c...
3adant1 1131 Deduction adding a conjunc...
3adant2 1132 Deduction adding a conjunc...
3adant3 1133 Deduction adding a conjunc...
3ad2ant1 1134 Deduction adding conjuncts...
3ad2ant2 1135 Deduction adding conjuncts...
3ad2ant3 1136 Deduction adding conjuncts...
simp1 1137 Simplification of triple c...
simp2 1138 Simplification of triple c...
simp3 1139 Simplification of triple c...
simp1i 1140 Infer a conjunct from a tr...
simp2i 1141 Infer a conjunct from a tr...
simp3i 1142 Infer a conjunct from a tr...
simp1d 1143 Deduce a conjunct from a t...
simp2d 1144 Deduce a conjunct from a t...
simp3d 1145 Deduce a conjunct from a t...
simp1bi 1146 Deduce a conjunct from a t...
simp2bi 1147 Deduce a conjunct from a t...
simp3bi 1148 Deduce a conjunct from a t...
3simpa 1149 Simplification of triple c...
3simpb 1150 Simplification of triple c...
3simpc 1151 Simplification of triple c...
3anim123i 1152 Join antecedents and conse...
3anim1i 1153 Add two conjuncts to antec...
3anim2i 1154 Add two conjuncts to antec...
3anim3i 1155 Add two conjuncts to antec...
3anbi123i 1156 Join 3 biconditionals with...
3orbi123i 1157 Join 3 biconditionals with...
3anbi1i 1158 Inference adding two conju...
3anbi2i 1159 Inference adding two conju...
3anbi3i 1160 Inference adding two conju...
syl3an 1161 A triple syllogism inferen...
syl3anb 1162 A triple syllogism inferen...
syl3anbr 1163 A triple syllogism inferen...
syl3an1 1164 A syllogism inference. (C...
syl3an2 1165 A syllogism inference. (C...
syl3an3 1166 A syllogism inference. (C...
3adantl1 1167 Deduction adding a conjunc...
3adantl2 1168 Deduction adding a conjunc...
3adantl3 1169 Deduction adding a conjunc...
3adantr1 1170 Deduction adding a conjunc...
3adantr2 1171 Deduction adding a conjunc...
3adantr3 1172 Deduction adding a conjunc...
ad4ant123 1173 Deduction adding conjuncts...
ad4ant124 1174 Deduction adding conjuncts...
ad4ant134 1175 Deduction adding conjuncts...
ad4ant234 1176 Deduction adding conjuncts...
3adant1l 1177 Deduction adding a conjunc...
3adant1r 1178 Deduction adding a conjunc...
3adant2l 1179 Deduction adding a conjunc...
3adant2r 1180 Deduction adding a conjunc...
3adant3l 1181 Deduction adding a conjunc...
3adant3r 1182 Deduction adding a conjunc...
3adant3r1 1183 Deduction adding a conjunc...
3adant3r2 1184 Deduction adding a conjunc...
3adant3r3 1185 Deduction adding a conjunc...
3ad2antl1 1186 Deduction adding conjuncts...
3ad2antl2 1187 Deduction adding conjuncts...
3ad2antl3 1188 Deduction adding conjuncts...
3ad2antr1 1189 Deduction adding conjuncts...
3ad2antr2 1190 Deduction adding conjuncts...
3ad2antr3 1191 Deduction adding conjuncts...
simpl1 1192 Simplification of conjunct...
simpl2 1193 Simplification of conjunct...
simpl3 1194 Simplification of conjunct...
simpr1 1195 Simplification of conjunct...
simpr2 1196 Simplification of conjunct...
simpr3 1197 Simplification of conjunct...
simp1l 1198 Simplification of triple c...
simp1r 1199 Simplification of triple c...
simp2l 1200 Simplification of triple c...
simp2r 1201 Simplification of triple c...
simp3l 1202 Simplification of triple c...
simp3r 1203 Simplification of triple c...
simp11 1204 Simplification of doubly t...
simp12 1205 Simplification of doubly t...
simp13 1206 Simplification of doubly t...
simp21 1207 Simplification of doubly t...
simp22 1208 Simplification of doubly t...
simp23 1209 Simplification of doubly t...
simp31 1210 Simplification of doubly t...
simp32 1211 Simplification of doubly t...
simp33 1212 Simplification of doubly t...
simpll1 1213 Simplification of conjunct...
simpll2 1214 Simplification of conjunct...
simpll3 1215 Simplification of conjunct...
simplr1 1216 Simplification of conjunct...
simplr2 1217 Simplification of conjunct...
simplr3 1218 Simplification of conjunct...
simprl1 1219 Simplification of conjunct...
simprl2 1220 Simplification of conjunct...
simprl3 1221 Simplification of conjunct...
simprr1 1222 Simplification of conjunct...
simprr2 1223 Simplification of conjunct...
simprr3 1224 Simplification of conjunct...
simpl1l 1225 Simplification of conjunct...
simpl1r 1226 Simplification of conjunct...
simpl2l 1227 Simplification of conjunct...
simpl2r 1228 Simplification of conjunct...
simpl3l 1229 Simplification of conjunct...
simpl3r 1230 Simplification of conjunct...
simpr1l 1231 Simplification of conjunct...
simpr1r 1232 Simplification of conjunct...
simpr2l 1233 Simplification of conjunct...
simpr2r 1234 Simplification of conjunct...
simpr3l 1235 Simplification of conjunct...
simpr3r 1236 Simplification of conjunct...
simp1ll 1237 Simplification of conjunct...
simp1lr 1238 Simplification of conjunct...
simp1rl 1239 Simplification of conjunct...
simp1rr 1240 Simplification of conjunct...
simp2ll 1241 Simplification of conjunct...
simp2lr 1242 Simplification of conjunct...
simp2rl 1243 Simplification of conjunct...
simp2rr 1244 Simplification of conjunct...
simp3ll 1245 Simplification of conjunct...
simp3lr 1246 Simplification of conjunct...
simp3rl 1247 Simplification of conjunct...
simp3rr 1248 Simplification of conjunct...
simpl11 1249 Simplification of conjunct...
simpl12 1250 Simplification of conjunct...
simpl13 1251 Simplification of conjunct...
simpl21 1252 Simplification of conjunct...
simpl22 1253 Simplification of conjunct...
simpl23 1254 Simplification of conjunct...
simpl31 1255 Simplification of conjunct...
simpl32 1256 Simplification of conjunct...
simpl33 1257 Simplification of conjunct...
simpr11 1258 Simplification of conjunct...
simpr12 1259 Simplification of conjunct...
simpr13 1260 Simplification of conjunct...
simpr21 1261 Simplification of conjunct...
simpr22 1262 Simplification of conjunct...
simpr23 1263 Simplification of conjunct...
simpr31 1264 Simplification of conjunct...
simpr32 1265 Simplification of conjunct...
simpr33 1266 Simplification of conjunct...
simp1l1 1267 Simplification of conjunct...
simp1l2 1268 Simplification of conjunct...
simp1l3 1269 Simplification of conjunct...
simp1r1 1270 Simplification of conjunct...
simp1r2 1271 Simplification of conjunct...
simp1r3 1272 Simplification of conjunct...
simp2l1 1273 Simplification of conjunct...
simp2l2 1274 Simplification of conjunct...
simp2l3 1275 Simplification of conjunct...
simp2r1 1276 Simplification of conjunct...
simp2r2 1277 Simplification of conjunct...
simp2r3 1278 Simplification of conjunct...
simp3l1 1279 Simplification of conjunct...
simp3l2 1280 Simplification of conjunct...
simp3l3 1281 Simplification of conjunct...
simp3r1 1282 Simplification of conjunct...
simp3r2 1283 Simplification of conjunct...
simp3r3 1284 Simplification of conjunct...
simp11l 1285 Simplification of conjunct...
simp11r 1286 Simplification of conjunct...
simp12l 1287 Simplification of conjunct...
simp12r 1288 Simplification of conjunct...
simp13l 1289 Simplification of conjunct...
simp13r 1290 Simplification of conjunct...
simp21l 1291 Simplification of conjunct...
simp21r 1292 Simplification of conjunct...
simp22l 1293 Simplification of conjunct...
simp22r 1294 Simplification of conjunct...
simp23l 1295 Simplification of conjunct...
simp23r 1296 Simplification of conjunct...
simp31l 1297 Simplification of conjunct...
simp31r 1298 Simplification of conjunct...
simp32l 1299 Simplification of conjunct...
simp32r 1300 Simplification of conjunct...
simp33l 1301 Simplification of conjunct...
simp33r 1302 Simplification of conjunct...
simp111 1303 Simplification of conjunct...
simp112 1304 Simplification of conjunct...
simp113 1305 Simplification of conjunct...
simp121 1306 Simplification of conjunct...
simp122 1307 Simplification of conjunct...
simp123 1308 Simplification of conjunct...
simp131 1309 Simplification of conjunct...
simp132 1310 Simplification of conjunct...
simp133 1311 Simplification of conjunct...
simp211 1312 Simplification of conjunct...
simp212 1313 Simplification of conjunct...
simp213 1314 Simplification of conjunct...
simp221 1315 Simplification of conjunct...
simp222 1316 Simplification of conjunct...
simp223 1317 Simplification of conjunct...
simp231 1318 Simplification of conjunct...
simp232 1319 Simplification of conjunct...
simp233 1320 Simplification of conjunct...
simp311 1321 Simplification of conjunct...
simp312 1322 Simplification of conjunct...
simp313 1323 Simplification of conjunct...
simp321 1324 Simplification of conjunct...
simp322 1325 Simplification of conjunct...
simp323 1326 Simplification of conjunct...
simp331 1327 Simplification of conjunct...
simp332 1328 Simplification of conjunct...
simp333 1329 Simplification of conjunct...
3anibar 1330 Remove a hypothesis from t...
3mix1 1331 Introduction in triple dis...
3mix2 1332 Introduction in triple dis...
3mix3 1333 Introduction in triple dis...
3mix1i 1334 Introduction in triple dis...
3mix2i 1335 Introduction in triple dis...
3mix3i 1336 Introduction in triple dis...
3mix1d 1337 Deduction introducing trip...
3mix2d 1338 Deduction introducing trip...
3mix3d 1339 Deduction introducing trip...
3pm3.2i 1340 Infer conjunction of premi...
pm3.2an3 1341 Version of ~ pm3.2 for a t...
mpbir3an 1342 Detach a conjunction of tr...
mpbir3and 1343 Detach a conjunction of tr...
syl3anbrc 1344 Syllogism inference. (Con...
syl21anbrc 1345 Syllogism inference. (Con...
3imp3i2an 1346 An elimination deduction. ...
ex3 1347 Apply ~ ex to a hypothesis...
3imp1 1348 Importation to left triple...
3impd 1349 Importation deduction for ...
3imp2 1350 Importation to right tripl...
3impdi 1351 Importation inference (und...
3impdir 1352 Importation inference (und...
3exp1 1353 Exportation from left trip...
3expd 1354 Exportation deduction for ...
3exp2 1355 Exportation from right tri...
exp5o 1356 A triple exportation infer...
exp516 1357 A triple exportation infer...
exp520 1358 A triple exportation infer...
3impexp 1359 Version of ~ impexp for a ...
3an1rs 1360 Swap conjuncts. (Contribu...
3anassrs 1361 Associative law for conjun...
ad5ant245 1362 Deduction adding conjuncts...
ad5ant234 1363 Deduction adding conjuncts...
ad5ant235 1364 Deduction adding conjuncts...
ad5ant123 1365 Deduction adding conjuncts...
ad5ant124 1366 Deduction adding conjuncts...
ad5ant125 1367 Deduction adding conjuncts...
ad5ant134 1368 Deduction adding conjuncts...
ad5ant135 1369 Deduction adding conjuncts...
ad5ant145 1370 Deduction adding conjuncts...
ad5ant2345 1371 Deduction adding conjuncts...
syl3anc 1372 Syllogism combined with co...
syl13anc 1373 Syllogism combined with co...
syl31anc 1374 Syllogism combined with co...
syl112anc 1375 Syllogism combined with co...
syl121anc 1376 Syllogism combined with co...
syl211anc 1377 Syllogism combined with co...
syl23anc 1378 Syllogism combined with co...
syl32anc 1379 Syllogism combined with co...
syl122anc 1380 Syllogism combined with co...
syl212anc 1381 Syllogism combined with co...
syl221anc 1382 Syllogism combined with co...
syl113anc 1383 Syllogism combined with co...
syl131anc 1384 Syllogism combined with co...
syl311anc 1385 Syllogism combined with co...
syl33anc 1386 Syllogism combined with co...
syl222anc 1387 Syllogism combined with co...
syl123anc 1388 Syllogism combined with co...
syl132anc 1389 Syllogism combined with co...
syl213anc 1390 Syllogism combined with co...
syl231anc 1391 Syllogism combined with co...
syl312anc 1392 Syllogism combined with co...
syl321anc 1393 Syllogism combined with co...
syl133anc 1394 Syllogism combined with co...
syl313anc 1395 Syllogism combined with co...
syl331anc 1396 Syllogism combined with co...
syl223anc 1397 Syllogism combined with co...
syl232anc 1398 Syllogism combined with co...
syl322anc 1399 Syllogism combined with co...
syl233anc 1400 Syllogism combined with co...
syl323anc 1401 Syllogism combined with co...
syl332anc 1402 Syllogism combined with co...
syl333anc 1403 A syllogism inference comb...
syl3an1b 1404 A syllogism inference. (C...
syl3an2b 1405 A syllogism inference. (C...
syl3an3b 1406 A syllogism inference. (C...
syl3an1br 1407 A syllogism inference. (C...
syl3an2br 1408 A syllogism inference. (C...
syl3an3br 1409 A syllogism inference. (C...
syld3an3 1410 A syllogism inference. (C...
syld3an1 1411 A syllogism inference. (C...
syld3an2 1412 A syllogism inference. (C...
syl3anl1 1413 A syllogism inference. (C...
syl3anl2 1414 A syllogism inference. (C...
syl3anl3 1415 A syllogism inference. (C...
syl3anl 1416 A triple syllogism inferen...
syl3anr1 1417 A syllogism inference. (C...
syl3anr2 1418 A syllogism inference. (C...
syl3anr3 1419 A syllogism inference. (C...
3anidm12 1420 Inference from idempotent ...
3anidm13 1421 Inference from idempotent ...
3anidm23 1422 Inference from idempotent ...
syl2an3an 1423 ~ syl3an with antecedents ...
syl2an23an 1424 Deduction related to ~ syl...
3ori 1425 Infer implication from tri...
3jao 1426 Disjunction of three antec...
3jaob 1427 Disjunction of three antec...
3jaoi 1428 Disjunction of three antec...
3jaod 1429 Disjunction of three antec...
3jaoian 1430 Disjunction of three antec...
3jaodan 1431 Disjunction of three antec...
mpjao3dan 1432 Eliminate a three-way disj...
mpjao3danOLD 1433 Obsolete version of ~ mpja...
3jaao 1434 Inference conjoining and d...
syl3an9b 1435 Nested syllogism inference...
3orbi123d 1436 Deduction joining 3 equiva...
3anbi123d 1437 Deduction joining 3 equiva...
3anbi12d 1438 Deduction conjoining and a...
3anbi13d 1439 Deduction conjoining and a...
3anbi23d 1440 Deduction conjoining and a...
3anbi1d 1441 Deduction adding conjuncts...
3anbi2d 1442 Deduction adding conjuncts...
3anbi3d 1443 Deduction adding conjuncts...
3anim123d 1444 Deduction joining 3 implic...
3orim123d 1445 Deduction joining 3 implic...
an6 1446 Rearrangement of 6 conjunc...
3an6 1447 Analogue of ~ an4 for trip...
3or6 1448 Analogue of ~ or4 for trip...
mp3an1 1449 An inference based on modu...
mp3an2 1450 An inference based on modu...
mp3an3 1451 An inference based on modu...
mp3an12 1452 An inference based on modu...
mp3an13 1453 An inference based on modu...
mp3an23 1454 An inference based on modu...
mp3an1i 1455 An inference based on modu...
mp3anl1 1456 An inference based on modu...
mp3anl2 1457 An inference based on modu...
mp3anl3 1458 An inference based on modu...
mp3anr1 1459 An inference based on modu...
mp3anr2 1460 An inference based on modu...
mp3anr3 1461 An inference based on modu...
mp3an 1462 An inference based on modu...
mpd3an3 1463 An inference based on modu...
mpd3an23 1464 An inference based on modu...
mp3and 1465 A deduction based on modus...
mp3an12i 1466 ~ mp3an with antecedents i...
mp3an2i 1467 ~ mp3an with antecedents i...
mp3an3an 1468 ~ mp3an with antecedents i...
mp3an2ani 1469 An elimination deduction. ...
biimp3a 1470 Infer implication from a l...
biimp3ar 1471 Infer implication from a l...
3anandis 1472 Inference that undistribut...
3anandirs 1473 Inference that undistribut...
ecase23d 1474 Deduction for elimination ...
3ecase 1475 Inference for elimination ...
3bior1fd 1476 A disjunction is equivalen...
3bior1fand 1477 A disjunction is equivalen...
3bior2fd 1478 A wff is equivalent to its...
3biant1d 1479 A conjunction is equivalen...
intn3an1d 1480 Introduction of a triple c...
intn3an2d 1481 Introduction of a triple c...
intn3an3d 1482 Introduction of a triple c...
an3andi 1483 Distribution of conjunctio...
an33rean 1484 Rearrange a 9-fold conjunc...
an33reanOLD 1485 Obsolete version of ~ an33...
nanan 1488 Conjunction in terms of al...
dfnan2 1489 Alternative denial in term...
nanor 1490 Alternative denial in term...
nancom 1491 Alternative denial is comm...
nannan 1492 Nested alternative denials...
nanim 1493 Implication in terms of al...
nannot 1494 Negation in terms of alter...
nanbi 1495 Biconditional in terms of ...
nanbi1 1496 Introduce a right anti-con...
nanbi2 1497 Introduce a left anti-conj...
nanbi12 1498 Join two logical equivalen...
nanbi1i 1499 Introduce a right anti-con...
nanbi2i 1500 Introduce a left anti-conj...
nanbi12i 1501 Join two logical equivalen...
nanbi1d 1502 Introduce a right anti-con...
nanbi2d 1503 Introduce a left anti-conj...
nanbi12d 1504 Join two logical equivalen...
nanass 1505 A characterization of when...
xnor 1508 Two ways to write XNOR (ex...
xorcom 1509 The connector ` \/_ ` is c...
xorcomOLD 1510 Obsolete version of ~ xorc...
xorass 1511 The connector ` \/_ ` is a...
excxor 1512 This tautology shows that ...
xor2 1513 Two ways to express "exclu...
xoror 1514 Exclusive disjunction impl...
xornan 1515 Exclusive disjunction impl...
xornan2 1516 XOR implies NAND (written ...
xorneg2 1517 The connector ` \/_ ` is n...
xorneg1 1518 The connector ` \/_ ` is n...
xorneg 1519 The connector ` \/_ ` is u...
xorbi12i 1520 Equality property for excl...
xorbi12iOLD 1521 Obsolete version of ~ xorb...
xorbi12d 1522 Equality property for excl...
anxordi 1523 Conjunction distributes ov...
xorexmid 1524 Exclusive-or variant of th...
norcom 1527 The connector ` -\/ ` is c...
norcomOLD 1528 Obsolete version of ~ norc...
nornot 1529 ` -. ` is expressible via ...
nornotOLD 1530 Obsolete version of ~ norn...
noran 1531 ` /\ ` is expressible via ...
noranOLD 1532 Obsolete version of ~ nora...
noror 1533 ` \/ ` is expressible via ...
nororOLD 1534 Obsolete version of ~ noro...
norasslem1 1535 This lemma shows the equiv...
norasslem2 1536 This lemma specializes ~ b...
norasslem3 1537 This lemma specializes ~ b...
norass 1538 A characterization of when...
norassOLD 1539 Obsolete version of ~ nora...
trujust 1544 Soundness justification th...
tru 1546 The truth value ` T. ` is ...
dftru2 1547 An alternate definition of...
trut 1548 A proposition is equivalen...
mptru 1549 Eliminate ` T. ` as an ant...
tbtru 1550 A proposition is equivalen...
bitru 1551 A theorem is equivalent to...
trud 1552 Anything implies ` T. ` . ...
truan 1553 True can be removed from a...
fal 1556 The truth value ` F. ` is ...
nbfal 1557 The negation of a proposit...
bifal 1558 A contradiction is equival...
falim 1559 The truth value ` F. ` imp...
falimd 1560 The truth value ` F. ` imp...
dfnot 1561 Given falsum ` F. ` , we c...
inegd 1562 Negation introduction rule...
efald 1563 Deduction based on reducti...
pm2.21fal 1564 If a wff and its negation ...
truimtru 1565 A ` -> ` identity. (Contr...
truimfal 1566 A ` -> ` identity. (Contr...
falimtru 1567 A ` -> ` identity. (Contr...
falimfal 1568 A ` -> ` identity. (Contr...
nottru 1569 A ` -. ` identity. (Contr...
notfal 1570 A ` -. ` identity. (Contr...
trubitru 1571 A ` <-> ` identity. (Cont...
falbitru 1572 A ` <-> ` identity. (Cont...
trubifal 1573 A ` <-> ` identity. (Cont...
falbifal 1574 A ` <-> ` identity. (Cont...
truantru 1575 A ` /\ ` identity. (Contr...
truanfal 1576 A ` /\ ` identity. (Contr...
falantru 1577 A ` /\ ` identity. (Contr...
falanfal 1578 A ` /\ ` identity. (Contr...
truortru 1579 A ` \/ ` identity. (Contr...
truorfal 1580 A ` \/ ` identity. (Contr...
falortru 1581 A ` \/ ` identity. (Contr...
falorfal 1582 A ` \/ ` identity. (Contr...
trunantru 1583 A ` -/\ ` identity. (Cont...
trunanfal 1584 A ` -/\ ` identity. (Cont...
falnantru 1585 A ` -/\ ` identity. (Cont...
falnanfal 1586 A ` -/\ ` identity. (Cont...
truxortru 1587 A ` \/_ ` identity. (Cont...
truxorfal 1588 A ` \/_ ` identity. (Cont...
falxortru 1589 A ` \/_ ` identity. (Cont...
falxorfal 1590 A ` \/_ ` identity. (Cont...
trunortru 1591 A ` -\/ ` identity. (Cont...
trunortruOLD 1592 Obsolete version of ~ trun...
trunorfal 1593 A ` -\/ ` identity. (Cont...
trunorfalOLD 1594 Obsolete version of ~ trun...
falnortru 1595 A ` -\/ ` identity. (Cont...
falnorfal 1596 A ` -\/ ` identity. (Cont...
falnorfalOLD 1597 Obsolete version of ~ faln...
hadbi123d 1600 Equality theorem for the a...
hadbi123i 1601 Equality theorem for the a...
hadass 1602 Associative law for the ad...
hadbi 1603 The adder sum is the same ...
hadcoma 1604 Commutative law for the ad...
hadcomaOLD 1605 Obsolete version of ~ hadc...
hadcomb 1606 Commutative law for the ad...
hadrot 1607 Rotation law for the adder...
hadnot 1608 The adder sum distributes ...
had1 1609 If the first input is true...
had0 1610 If the first input is fals...
hadifp 1611 The value of the adder sum...
cador 1614 The adder carry in disjunc...
cadan 1615 The adder carry in conjunc...
cadbi123d 1616 Equality theorem for the a...
cadbi123i 1617 Equality theorem for the a...
cadcoma 1618 Commutative law for the ad...
cadcomb 1619 Commutative law for the ad...
cadrot 1620 Rotation law for the adder...
cadnot 1621 The adder carry distribute...
cad11 1622 If (at least) two inputs a...
cad1 1623 If one input is true, then...
cad0 1624 If one input is false, the...
cad0OLD 1625 Obsolete version of ~ cad0...
cadifp 1626 The value of the carry is,...
cadtru 1627 The adder carry is true as...
minimp 1628 A single axiom for minimal...
minimp-syllsimp 1629 Derivation of Syll-Simp ( ...
minimp-ax1 1630 Derivation of ~ ax-1 from ...
minimp-ax2c 1631 Derivation of a commuted f...
minimp-ax2 1632 Derivation of ~ ax-2 from ...
minimp-pm2.43 1633 Derivation of ~ pm2.43 (al...
impsingle 1634 The shortest single axiom ...
impsingle-step4 1635 Derivation of impsingle-st...
impsingle-step8 1636 Derivation of impsingle-st...
impsingle-ax1 1637 Derivation of impsingle-ax...
impsingle-step15 1638 Derivation of impsingle-st...
impsingle-step18 1639 Derivation of impsingle-st...
impsingle-step19 1640 Derivation of impsingle-st...
impsingle-step20 1641 Derivation of impsingle-st...
impsingle-step21 1642 Derivation of impsingle-st...
impsingle-step22 1643 Derivation of impsingle-st...
impsingle-step25 1644 Derivation of impsingle-st...
impsingle-imim1 1645 Derivation of impsingle-im...
impsingle-peirce 1646 Derivation of impsingle-pe...
tarski-bernays-ax2 1647 Derivation of ~ ax-2 from ...
meredith 1648 Carew Meredith's sole axio...
merlem1 1649 Step 3 of Meredith's proof...
merlem2 1650 Step 4 of Meredith's proof...
merlem3 1651 Step 7 of Meredith's proof...
merlem4 1652 Step 8 of Meredith's proof...
merlem5 1653 Step 11 of Meredith's proo...
merlem6 1654 Step 12 of Meredith's proo...
merlem7 1655 Between steps 14 and 15 of...
merlem8 1656 Step 15 of Meredith's proo...
merlem9 1657 Step 18 of Meredith's proo...
merlem10 1658 Step 19 of Meredith's proo...
merlem11 1659 Step 20 of Meredith's proo...
merlem12 1660 Step 28 of Meredith's proo...
merlem13 1661 Step 35 of Meredith's proo...
luk-1 1662 1 of 3 axioms for proposit...
luk-2 1663 2 of 3 axioms for proposit...
luk-3 1664 3 of 3 axioms for proposit...
luklem1 1665 Used to rederive standard ...
luklem2 1666 Used to rederive standard ...
luklem3 1667 Used to rederive standard ...
luklem4 1668 Used to rederive standard ...
luklem5 1669 Used to rederive standard ...
luklem6 1670 Used to rederive standard ...
luklem7 1671 Used to rederive standard ...
luklem8 1672 Used to rederive standard ...
ax1 1673 Standard propositional axi...
ax2 1674 Standard propositional axi...
ax3 1675 Standard propositional axi...
nic-dfim 1676 This theorem "defines" imp...
nic-dfneg 1677 This theorem "defines" neg...
nic-mp 1678 Derive Nicod's rule of mod...
nic-mpALT 1679 A direct proof of ~ nic-mp...
nic-ax 1680 Nicod's axiom derived from...
nic-axALT 1681 A direct proof of ~ nic-ax...
nic-imp 1682 Inference for ~ nic-mp usi...
nic-idlem1 1683 Lemma for ~ nic-id . (Con...
nic-idlem2 1684 Lemma for ~ nic-id . Infe...
nic-id 1685 Theorem ~ id expressed wit...
nic-swap 1686 The connector ` -/\ ` is s...
nic-isw1 1687 Inference version of ~ nic...
nic-isw2 1688 Inference for swapping nes...
nic-iimp1 1689 Inference version of ~ nic...
nic-iimp2 1690 Inference version of ~ nic...
nic-idel 1691 Inference to remove the tr...
nic-ich 1692 Chained inference. (Contr...
nic-idbl 1693 Double the terms. Since d...
nic-bijust 1694 Biconditional justificatio...
nic-bi1 1695 Inference to extract one s...
nic-bi2 1696 Inference to extract the o...
nic-stdmp 1697 Derive the standard modus ...
nic-luk1 1698 Proof of ~ luk-1 from ~ ni...
nic-luk2 1699 Proof of ~ luk-2 from ~ ni...
nic-luk3 1700 Proof of ~ luk-3 from ~ ni...
lukshef-ax1 1701 This alternative axiom for...
lukshefth1 1702 Lemma for ~ renicax . (Co...
lukshefth2 1703 Lemma for ~ renicax . (Co...
renicax 1704 A rederivation of ~ nic-ax...
tbw-bijust 1705 Justification for ~ tbw-ne...
tbw-negdf 1706 The definition of negation...
tbw-ax1 1707 The first of four axioms i...
tbw-ax2 1708 The second of four axioms ...
tbw-ax3 1709 The third of four axioms i...
tbw-ax4 1710 The fourth of four axioms ...
tbwsyl 1711 Used to rederive the Lukas...
tbwlem1 1712 Used to rederive the Lukas...
tbwlem2 1713 Used to rederive the Lukas...
tbwlem3 1714 Used to rederive the Lukas...
tbwlem4 1715 Used to rederive the Lukas...
tbwlem5 1716 Used to rederive the Lukas...
re1luk1 1717 ~ luk-1 derived from the T...
re1luk2 1718 ~ luk-2 derived from the T...
re1luk3 1719 ~ luk-3 derived from the T...
merco1 1720 A single axiom for proposi...
merco1lem1 1721 Used to rederive the Tarsk...
retbwax4 1722 ~ tbw-ax4 rederived from ~...
retbwax2 1723 ~ tbw-ax2 rederived from ~...
merco1lem2 1724 Used to rederive the Tarsk...
merco1lem3 1725 Used to rederive the Tarsk...
merco1lem4 1726 Used to rederive the Tarsk...
merco1lem5 1727 Used to rederive the Tarsk...
merco1lem6 1728 Used to rederive the Tarsk...
merco1lem7 1729 Used to rederive the Tarsk...
retbwax3 1730 ~ tbw-ax3 rederived from ~...
merco1lem8 1731 Used to rederive the Tarsk...
merco1lem9 1732 Used to rederive the Tarsk...
merco1lem10 1733 Used to rederive the Tarsk...
merco1lem11 1734 Used to rederive the Tarsk...
merco1lem12 1735 Used to rederive the Tarsk...
merco1lem13 1736 Used to rederive the Tarsk...
merco1lem14 1737 Used to rederive the Tarsk...
merco1lem15 1738 Used to rederive the Tarsk...
merco1lem16 1739 Used to rederive the Tarsk...
merco1lem17 1740 Used to rederive the Tarsk...
merco1lem18 1741 Used to rederive the Tarsk...
retbwax1 1742 ~ tbw-ax1 rederived from ~...
merco2 1743 A single axiom for proposi...
mercolem1 1744 Used to rederive the Tarsk...
mercolem2 1745 Used to rederive the Tarsk...
mercolem3 1746 Used to rederive the Tarsk...
mercolem4 1747 Used to rederive the Tarsk...
mercolem5 1748 Used to rederive the Tarsk...
mercolem6 1749 Used to rederive the Tarsk...
mercolem7 1750 Used to rederive the Tarsk...
mercolem8 1751 Used to rederive the Tarsk...
re1tbw1 1752 ~ tbw-ax1 rederived from ~...
re1tbw2 1753 ~ tbw-ax2 rederived from ~...
re1tbw3 1754 ~ tbw-ax3 rederived from ~...
re1tbw4 1755 ~ tbw-ax4 rederived from ~...
rb-bijust 1756 Justification for ~ rb-imd...
rb-imdf 1757 The definition of implicat...
anmp 1758 Modus ponens for ` { \/ , ...
rb-ax1 1759 The first of four axioms i...
rb-ax2 1760 The second of four axioms ...
rb-ax3 1761 The third of four axioms i...
rb-ax4 1762 The fourth of four axioms ...
rbsyl 1763 Used to rederive the Lukas...
rblem1 1764 Used to rederive the Lukas...
rblem2 1765 Used to rederive the Lukas...
rblem3 1766 Used to rederive the Lukas...
rblem4 1767 Used to rederive the Lukas...
rblem5 1768 Used to rederive the Lukas...
rblem6 1769 Used to rederive the Lukas...
rblem7 1770 Used to rederive the Lukas...
re1axmp 1771 ~ ax-mp derived from Russe...
re2luk1 1772 ~ luk-1 derived from Russe...
re2luk2 1773 ~ luk-2 derived from Russe...
re2luk3 1774 ~ luk-3 derived from Russe...
mptnan 1775 Modus ponendo tollens 1, o...
mptxor 1776 Modus ponendo tollens 2, o...
mtpor 1777 Modus tollendo ponens (inc...
mtpxor 1778 Modus tollendo ponens (ori...
stoic1a 1779 Stoic logic Thema 1 (part ...
stoic1b 1780 Stoic logic Thema 1 (part ...
stoic2a 1781 Stoic logic Thema 2 versio...
stoic2b 1782 Stoic logic Thema 2 versio...
stoic3 1783 Stoic logic Thema 3. Stat...
stoic4a 1784 Stoic logic Thema 4 versio...
stoic4b 1785 Stoic logic Thema 4 versio...
alnex 1788 Universal quantification o...
eximal 1789 An equivalence between an ...
nf2 1792 Alternate definition of no...
nf3 1793 Alternate definition of no...
nf4 1794 Alternate definition of no...
nfi 1795 Deduce that ` x ` is not f...
nfri 1796 Consequence of the definit...
nfd 1797 Deduce that ` x ` is not f...
nfrd 1798 Consequence of the definit...
nftht 1799 Closed form of ~ nfth . (...
nfntht 1800 Closed form of ~ nfnth . ...
nfntht2 1801 Closed form of ~ nfnth . ...
gen2 1803 Generalization applied twi...
mpg 1804 Modus ponens combined with...
mpgbi 1805 Modus ponens on biconditio...
mpgbir 1806 Modus ponens on biconditio...
nex 1807 Generalization rule for ne...
nfth 1808 No variable is (effectivel...
nfnth 1809 No variable is (effectivel...
hbth 1810 No variable is (effectivel...
nftru 1811 The true constant has no f...
nffal 1812 The false constant has no ...
sptruw 1813 Version of ~ sp when ` ph ...
altru 1814 For all sets, ` T. ` is tr...
alfal 1815 For all sets, ` -. F. ` is...
alim 1817 Restatement of Axiom ~ ax-...
alimi 1818 Inference quantifying both...
2alimi 1819 Inference doubly quantifyi...
ala1 1820 Add an antecedent in a uni...
al2im 1821 Closed form of ~ al2imi . ...
al2imi 1822 Inference quantifying ante...
alanimi 1823 Variant of ~ al2imi with c...
alimdh 1824 Deduction form of Theorem ...
albi 1825 Theorem 19.15 of [Margaris...
albii 1826 Inference adding universal...
2albii 1827 Inference adding two unive...
sylgt 1828 Closed form of ~ sylg . (...
sylg 1829 A syllogism combined with ...
alrimih 1830 Inference form of Theorem ...
hbxfrbi 1831 A utility lemma to transfe...
alex 1832 Universal quantifier in te...
exnal 1833 Existential quantification...
2nalexn 1834 Part of theorem *11.5 in [...
2exnaln 1835 Theorem *11.22 in [Whitehe...
2nexaln 1836 Theorem *11.25 in [Whitehe...
alimex 1837 An equivalence between an ...
aleximi 1838 A variant of ~ al2imi : in...
alexbii 1839 Biconditional form of ~ al...
exim 1840 Theorem 19.22 of [Margaris...
eximi 1841 Inference adding existenti...
2eximi 1842 Inference adding two exist...
eximii 1843 Inference associated with ...
exa1 1844 Add an antecedent in an ex...
19.38 1845 Theorem 19.38 of [Margaris...
19.38a 1846 Under a nonfreeness hypoth...
19.38b 1847 Under a nonfreeness hypoth...
imnang 1848 Quantified implication in ...
alinexa 1849 A transformation of quanti...
exnalimn 1850 Existential quantification...
alexn 1851 A relationship between two...
2exnexn 1852 Theorem *11.51 in [Whitehe...
exbi 1853 Theorem 19.18 of [Margaris...
exbii 1854 Inference adding existenti...
2exbii 1855 Inference adding two exist...
3exbii 1856 Inference adding three exi...
nfbiit 1857 Equivalence theorem for th...
nfbii 1858 Equality theorem for the n...
nfxfr 1859 A utility lemma to transfe...
nfxfrd 1860 A utility lemma to transfe...
nfnbi 1861 A variable is nonfree in a...
nfnt 1862 If a variable is nonfree i...
nfn 1863 Inference associated with ...
nfnd 1864 Deduction associated with ...
exanali 1865 A transformation of quanti...
2exanali 1866 Theorem *11.521 in [Whiteh...
exancom 1867 Commutation of conjunction...
exan 1868 Place a conjunct in the sc...
alrimdh 1869 Deduction form of Theorem ...
eximdh 1870 Deduction from Theorem 19....
nexdh 1871 Deduction for generalizati...
albidh 1872 Formula-building rule for ...
exbidh 1873 Formula-building rule for ...
exsimpl 1874 Simplification of an exist...
exsimpr 1875 Simplification of an exist...
19.26 1876 Theorem 19.26 of [Margaris...
19.26-2 1877 Theorem ~ 19.26 with two q...
19.26-3an 1878 Theorem ~ 19.26 with tripl...
19.29 1879 Theorem 19.29 of [Margaris...
19.29r 1880 Variation of ~ 19.29 . (C...
19.29r2 1881 Variation of ~ 19.29r with...
19.29x 1882 Variation of ~ 19.29 with ...
19.35 1883 Theorem 19.35 of [Margaris...
19.35i 1884 Inference associated with ...
19.35ri 1885 Inference associated with ...
19.25 1886 Theorem 19.25 of [Margaris...
19.30 1887 Theorem 19.30 of [Margaris...
19.43 1888 Theorem 19.43 of [Margaris...
19.43OLD 1889 Obsolete proof of ~ 19.43 ...
19.33 1890 Theorem 19.33 of [Margaris...
19.33b 1891 The antecedent provides a ...
19.40 1892 Theorem 19.40 of [Margaris...
19.40-2 1893 Theorem *11.42 in [Whitehe...
19.40b 1894 The antecedent provides a ...
albiim 1895 Split a biconditional and ...
2albiim 1896 Split a biconditional and ...
exintrbi 1897 Add/remove a conjunct in t...
exintr 1898 Introduce a conjunct in th...
alsyl 1899 Universally quantified and...
nfimd 1900 If in a context ` x ` is n...
nfimt 1901 Closed form of ~ nfim and ...
nfim 1902 If ` x ` is not free in ` ...
nfand 1903 If in a context ` x ` is n...
nf3and 1904 Deduction form of bound-va...
nfan 1905 If ` x ` is not free in ` ...
nfnan 1906 If ` x ` is not free in ` ...
nf3an 1907 If ` x ` is not free in ` ...
nfbid 1908 If in a context ` x ` is n...
nfbi 1909 If ` x ` is not free in ` ...
nfor 1910 If ` x ` is not free in ` ...
nf3or 1911 If ` x ` is not free in ` ...
empty 1912 Two characterizations of t...
emptyex 1913 On the empty domain, any e...
emptyal 1914 On the empty domain, any u...
emptynf 1915 On the empty domain, any v...
ax5d 1917 Version of ~ ax-5 with ant...
ax5e 1918 A rephrasing of ~ ax-5 usi...
ax5ea 1919 If a formula holds for som...
nfv 1920 If ` x ` is not present in...
nfvd 1921 ~ nfv with antecedent. Us...
alimdv 1922 Deduction form of Theorem ...
eximdv 1923 Deduction form of Theorem ...
2alimdv 1924 Deduction form of Theorem ...
2eximdv 1925 Deduction form of Theorem ...
albidv 1926 Formula-building rule for ...
exbidv 1927 Formula-building rule for ...
nfbidv 1928 An equality theorem for no...
2albidv 1929 Formula-building rule for ...
2exbidv 1930 Formula-building rule for ...
3exbidv 1931 Formula-building rule for ...
4exbidv 1932 Formula-building rule for ...
alrimiv 1933 Inference form of Theorem ...
alrimivv 1934 Inference form of Theorem ...
alrimdv 1935 Deduction form of Theorem ...
exlimiv 1936 Inference form of Theorem ...
exlimiiv 1937 Inference (Rule C) associa...
exlimivv 1938 Inference form of Theorem ...
exlimdv 1939 Deduction form of Theorem ...
exlimdvv 1940 Deduction form of Theorem ...
exlimddv 1941 Existential elimination ru...
nexdv 1942 Deduction for generalizati...
2ax5 1943 Quantification of two vari...
stdpc5v 1944 Version of ~ stdpc5 with a...
19.21v 1945 Version of ~ 19.21 with a ...
19.32v 1946 Version of ~ 19.32 with a ...
19.31v 1947 Version of ~ 19.31 with a ...
19.23v 1948 Version of ~ 19.23 with a ...
19.23vv 1949 Theorem ~ 19.23v extended ...
pm11.53v 1950 Version of ~ pm11.53 with ...
19.36imv 1951 One direction of ~ 19.36v ...
19.36imvOLD 1952 Obsolete version of ~ 19.3...
19.36iv 1953 Inference associated with ...
19.37imv 1954 One direction of ~ 19.37v ...
19.37iv 1955 Inference associated with ...
19.41v 1956 Version of ~ 19.41 with a ...
19.41vv 1957 Version of ~ 19.41 with tw...
19.41vvv 1958 Version of ~ 19.41 with th...
19.41vvvv 1959 Version of ~ 19.41 with fo...
19.42v 1960 Version of ~ 19.42 with a ...
exdistr 1961 Distribution of existentia...
exdistrv 1962 Distribute a pair of exist...
4exdistrv 1963 Distribute two pairs of ex...
19.42vv 1964 Version of ~ 19.42 with tw...
exdistr2 1965 Distribution of existentia...
19.42vvv 1966 Version of ~ 19.42 with th...
3exdistr 1967 Distribution of existentia...
4exdistr 1968 Distribution of existentia...
weq 1969 Extend wff definition to i...
speimfw 1970 Specialization, with addit...
speimfwALT 1971 Alternate proof of ~ speim...
spimfw 1972 Specialization, with addit...
ax12i 1973 Inference that has ~ ax-12...
ax6v 1975 Axiom B7 of [Tarski] p. 75...
ax6ev 1976 At least one individual ex...
spimw 1977 Specialization. Lemma 8 o...
spimew 1978 Existential introduction, ...
spimehOLD 1979 Obsolete version of ~ spim...
speiv 1980 Inference from existential...
speivw 1981 Version of ~ spei with a d...
exgen 1982 Rule of existential genera...
exgenOLD 1983 Obsolete version of ~ exge...
extru 1984 There exists a variable su...
19.2 1985 Theorem 19.2 of [Margaris]...
19.2d 1986 Deduction associated with ...
19.8w 1987 Weak version of ~ 19.8a an...
spnfw 1988 Weak version of ~ sp . Us...
spvw 1989 Version of ~ sp when ` x `...
19.3v 1990 Version of ~ 19.3 with a d...
19.8v 1991 Version of ~ 19.8a with a ...
19.9v 1992 Version of ~ 19.9 with a d...
19.3vOLD 1993 Obsolete version of ~ 19.3...
spvwOLD 1994 Obsolete version of ~ spvw...
19.39 1995 Theorem 19.39 of [Margaris...
19.24 1996 Theorem 19.24 of [Margaris...
19.34 1997 Theorem 19.34 of [Margaris...
19.36v 1998 Version of ~ 19.36 with a ...
19.12vvv 1999 Version of ~ 19.12vv with ...
19.27v 2000 Version of ~ 19.27 with a ...
19.28v 2001 Version of ~ 19.28 with a ...
19.37v 2002 Version of ~ 19.37 with a ...
19.44v 2003 Version of ~ 19.44 with a ...
19.45v 2004 Version of ~ 19.45 with a ...
spimevw 2005 Existential introduction, ...
spimvw 2006 A weak form of specializat...
spvv 2007 Specialization, using impl...
spfalw 2008 Version of ~ sp when ` ph ...
chvarvv 2009 Implicit substitution of `...
equs4v 2010 Version of ~ equs4 with a ...
alequexv 2011 Version of ~ equs4v with i...
exsbim 2012 One direction of the equiv...
equsv 2013 If a formula does not cont...
equsalvw 2014 Version of ~ equsalv with ...
equsexvw 2015 Version of ~ equsexv with ...
equsexvwOLD 2016 Obsolete version of ~ equs...
cbvaliw 2017 Change bound variable. Us...
cbvalivw 2018 Change bound variable. Us...
ax7v 2020 Weakened version of ~ ax-7...
ax7v1 2021 First of two weakened vers...
ax7v2 2022 Second of two weakened ver...
equid 2023 Identity law for equality....
nfequid 2024 Bound-variable hypothesis ...
equcomiv 2025 Weaker form of ~ equcomi w...
ax6evr 2026 A commuted form of ~ ax6ev...
ax7 2027 Proof of ~ ax-7 from ~ ax7...
equcomi 2028 Commutative law for equali...
equcom 2029 Commutative law for equali...
equcomd 2030 Deduction form of ~ equcom...
equcoms 2031 An inference commuting equ...
equtr 2032 A transitive law for equal...
equtrr 2033 A transitive law for equal...
equeuclr 2034 Commuted version of ~ eque...
equeucl 2035 Equality is a left-Euclide...
equequ1 2036 An equivalence law for equ...
equequ2 2037 An equivalence law for equ...
equtr2 2038 Equality is a left-Euclide...
stdpc6 2039 One of the two equality ax...
equvinv 2040 A variable introduction la...
equvinva 2041 A modified version of the ...
equvelv 2042 A biconditional form of ~ ...
ax13b 2043 An equivalence between two...
spfw 2044 Weak version of ~ sp . Us...
spw 2045 Weak version of the specia...
cbvalw 2046 Change bound variable. Us...
cbvalvw 2047 Change bound variable. Us...
cbvexvw 2048 Change bound variable. Us...
cbvaldvaw 2049 Rule used to change the bo...
cbvexdvaw 2050 Rule used to change the bo...
cbval2vw 2051 Rule used to change bound ...
cbvex2vw 2052 Rule used to change bound ...
cbvex4vw 2053 Rule used to change bound ...
alcomiw 2054 Weak version of ~ alcom . ...
alcomiwOLD 2055 Obsolete version of ~ alco...
hbn1fw 2056 Weak version of ~ ax-10 fr...
hbn1w 2057 Weak version of ~ hbn1 . ...
hba1w 2058 Weak version of ~ hba1 . ...
hbe1w 2059 Weak version of ~ hbe1 . ...
hbalw 2060 Weak version of ~ hbal . ...
spaev 2061 A special instance of ~ sp...
cbvaev 2062 Change bound variable in a...
aevlem0 2063 Lemma for ~ aevlem . Inst...
aevlem 2064 Lemma for ~ aev and ~ axc1...
aeveq 2065 The antecedent ` A. x x = ...
aev 2066 A "distinctor elimination"...
aev2 2067 A version of ~ aev with tw...
hbaev 2068 All variables are effectiv...
naev 2069 If some set variables can ...
naev2 2070 Generalization of ~ hbnaev...
hbnaev 2071 Any variable is free in ` ...
sbjust 2072 Justification theorem for ...
sbt 2075 A substitution into a theo...
sbtru 2076 The result of substituting...
stdpc4 2077 The specialization axiom o...
sbtALT 2078 Alternate proof of ~ sbt ,...
2stdpc4 2079 A double specialization us...
sbi1 2080 Distribute substitution ov...
spsbim 2081 Distribute substitution ov...
spsbbi 2082 Biconditional property for...
sbimi 2083 Distribute substitution ov...
sb2imi 2084 Distribute substitution ov...
sbbii 2085 Infer substitution into bo...
2sbbii 2086 Infer double substitution ...
sbimdv 2087 Deduction substituting bot...
sbbidv 2088 Deduction substituting bot...
sban 2089 Conjunction inside and out...
sb3an 2090 Threefold conjunction insi...
spsbe 2091 Existential generalization...
sbequ 2092 Equality property for subs...
sbequi 2093 An equality theorem for su...
sb6 2094 Alternate definition of su...
2sb6 2095 Equivalence for double sub...
sb1v 2096 One direction of ~ sb5 , p...
sbv 2097 Substitution for a variabl...
sbcom4 2098 Commutativity law for subs...
pm11.07 2099 Axiom *11.07 in [Whitehead...
sbrimvlem 2100 Common proof template for ...
sbrimvw 2101 Substitution in an implica...
sbievw 2102 Conversion of implicit sub...
sbiedvw 2103 Conversion of implicit sub...
2sbievw 2104 Conversion of double impli...
sbcom3vv 2105 Substituting ` y ` for ` x...
sbievw2 2106 ~ sbievw applied twice, av...
sbco2vv 2107 A composition law for subs...
equsb3 2108 Substitution in an equalit...
equsb3r 2109 Substitution applied to th...
equsb1v 2110 Substitution applied to an...
nsb 2111 Any substitution in an alw...
sbn1 2112 One direction of ~ sbn , u...
wel 2114 Extend wff definition to i...
ax8v 2116 Weakened version of ~ ax-8...
ax8v1 2117 First of two weakened vers...
ax8v2 2118 Second of two weakened ver...
ax8 2119 Proof of ~ ax-8 from ~ ax8...
elequ1 2120 An identity law for the no...
elsb3 2121 Substitution applied to an...
cleljust 2122 When the class variables i...
ax9v 2124 Weakened version of ~ ax-9...
ax9v1 2125 First of two weakened vers...
ax9v2 2126 Second of two weakened ver...
ax9 2127 Proof of ~ ax-9 from ~ ax9...
elequ2 2128 An identity law for the no...
elsb4 2129 Substitution applied to an...
elequ2g 2130 A form of ~ elequ2 with a ...
ax6dgen 2131 Tarski's system uses the w...
ax10w 2132 Weak version of ~ ax-10 fr...
ax11w 2133 Weak version of ~ ax-11 fr...
ax11dgen 2134 Degenerate instance of ~ a...
ax12wlem 2135 Lemma for weak version of ...
ax12w 2136 Weak version of ~ ax-12 fr...
ax12dgen 2137 Degenerate instance of ~ a...
ax12wdemo 2138 Example of an application ...
ax13w 2139 Weak version (principal in...
ax13dgen1 2140 Degenerate instance of ~ a...
ax13dgen2 2141 Degenerate instance of ~ a...
ax13dgen3 2142 Degenerate instance of ~ a...
ax13dgen4 2143 Degenerate instance of ~ a...
hbn1 2145 Alias for ~ ax-10 to be us...
hbe1 2146 The setvar ` x ` is not fr...
hbe1a 2147 Dual statement of ~ hbe1 ....
nf5-1 2148 One direction of ~ nf5 can...
nf5i 2149 Deduce that ` x ` is not f...
nf5dh 2150 Deduce that ` x ` is not f...
nf5dv 2151 Apply the definition of no...
nfnaew 2152 All variables are effectiv...
nfnaewOLD 2153 Obsolete version of ~ nfna...
nfe1 2154 The setvar ` x ` is not fr...
nfa1 2155 The setvar ` x ` is not fr...
nfna1 2156 A convenience theorem part...
nfia1 2157 Lemma 23 of [Monk2] p. 114...
nfnf1 2158 The setvar ` x ` is not fr...
modal5 2159 The analogue in our predic...
nfs1v 2160 The setvar ` x ` is not fr...
alcoms 2162 Swap quantifiers in an ant...
alcom 2163 Theorem 19.5 of [Margaris]...
alrot3 2164 Theorem *11.21 in [Whitehe...
alrot4 2165 Rotate four universal quan...
sbal 2166 Move universal quantifier ...
sbalv 2167 Quantify with new variable...
sbcom2 2168 Commutativity law for subs...
excom 2169 Theorem 19.11 of [Margaris...
excomim 2170 One direction of Theorem 1...
excom13 2171 Swap 1st and 3rd existenti...
exrot3 2172 Rotate existential quantif...
exrot4 2173 Rotate existential quantif...
hbal 2174 If ` x ` is not free in ` ...
hbald 2175 Deduction form of bound-va...
hbsbw 2176 If ` z ` is not free in ` ...
nfa2 2177 Lemma 24 of [Monk2] p. 114...
ax12v 2179 This is essentially Axiom ...
ax12v2 2180 It is possible to remove a...
19.8a 2181 If a wff is true, it is tr...
19.8ad 2182 If a wff is true, it is tr...
sp 2183 Specialization. A univers...
spi 2184 Inference rule of universa...
sps 2185 Generalization of antecede...
2sp 2186 A double specialization (s...
spsd 2187 Deduction generalizing ant...
19.2g 2188 Theorem 19.2 of [Margaris]...
19.21bi 2189 Inference form of ~ 19.21 ...
19.21bbi 2190 Inference removing two uni...
19.23bi 2191 Inference form of Theorem ...
nexr 2192 Inference associated with ...
qexmid 2193 Quantified excluded middle...
nf5r 2194 Consequence of the definit...
nf5rOLD 2195 Obsolete version of ~ nfrd...
nf5ri 2196 Consequence of the definit...
nf5rd 2197 Consequence of the definit...
spimedv 2198 Deduction version of ~ spi...
spimefv 2199 Version of ~ spime with a ...
nfim1 2200 A closed form of ~ nfim . ...
nfan1 2201 A closed form of ~ nfan . ...
19.3t 2202 Closed form of ~ 19.3 and ...
19.3 2203 A wff may be quantified wi...
19.9d 2204 A deduction version of one...
19.9t 2205 Closed form of ~ 19.9 and ...
19.9 2206 A wff may be existentially...
19.21t 2207 Closed form of Theorem 19....
19.21 2208 Theorem 19.21 of [Margaris...
stdpc5 2209 An axiom scheme of standar...
19.21-2 2210 Version of ~ 19.21 with tw...
19.23t 2211 Closed form of Theorem 19....
19.23 2212 Theorem 19.23 of [Margaris...
alimd 2213 Deduction form of Theorem ...
alrimi 2214 Inference form of Theorem ...
alrimdd 2215 Deduction form of Theorem ...
alrimd 2216 Deduction form of Theorem ...
eximd 2217 Deduction form of Theorem ...
exlimi 2218 Inference associated with ...
exlimd 2219 Deduction form of Theorem ...
exlimimdd 2220 Existential elimination ru...
exlimdd 2221 Existential elimination ru...
nexd 2222 Deduction for generalizati...
albid 2223 Formula-building rule for ...
exbid 2224 Formula-building rule for ...
nfbidf 2225 An equality theorem for ef...
19.16 2226 Theorem 19.16 of [Margaris...
19.17 2227 Theorem 19.17 of [Margaris...
19.27 2228 Theorem 19.27 of [Margaris...
19.28 2229 Theorem 19.28 of [Margaris...
19.19 2230 Theorem 19.19 of [Margaris...
19.36 2231 Theorem 19.36 of [Margaris...
19.36i 2232 Inference associated with ...
19.37 2233 Theorem 19.37 of [Margaris...
19.32 2234 Theorem 19.32 of [Margaris...
19.31 2235 Theorem 19.31 of [Margaris...
19.41 2236 Theorem 19.41 of [Margaris...
19.42 2237 Theorem 19.42 of [Margaris...
19.44 2238 Theorem 19.44 of [Margaris...
19.45 2239 Theorem 19.45 of [Margaris...
spimfv 2240 Specialization, using impl...
chvarfv 2241 Implicit substitution of `...
cbv3v2 2242 Version of ~ cbv3 with two...
sbalex 2243 Equivalence of two ways to...
sb4av 2244 Version of ~ sb4a with a d...
sbimd 2245 Deduction substituting bot...
sbbid 2246 Deduction substituting bot...
2sbbid 2247 Deduction doubly substitut...
sbequ1 2248 An equality theorem for su...
sbequ2 2249 An equality theorem for su...
sbequ2OLD 2250 Obsolete version of ~ sbeq...
stdpc7 2251 One of the two equality ax...
sbequ12 2252 An equality theorem for su...
sbequ12r 2253 An equality theorem for su...
sbelx 2254 Elimination of substitutio...
sbequ12a 2255 An equality theorem for su...
sbid 2256 An identity theorem for su...
sbcov 2257 A composition law for subs...
sb6a 2258 Equivalence for substituti...
sbid2vw 2259 Reverting substitution yie...
axc16g 2260 Generalization of ~ axc16 ...
axc16 2261 Proof of older axiom ~ ax-...
axc16gb 2262 Biconditional strengthenin...
axc16nf 2263 If ~ dtru is false, then t...
axc11v 2264 Version of ~ axc11 with a ...
axc11rv 2265 Version of ~ axc11r with a...
drsb2 2266 Formula-building lemma for...
equsalv 2267 An equivalence related to ...
equsexv 2268 An equivalence related to ...
sbft 2269 Substitution has no effect...
sbf 2270 Substitution for a variabl...
sbf2 2271 Substitution has no effect...
sbh 2272 Substitution for a variabl...
hbs1 2273 The setvar ` x ` is not fr...
nfs1f 2274 If ` x ` is not free in ` ...
sb5 2275 Alternate definition of su...
sb5OLD 2276 Obsolete version of ~ sb5 ...
sb56OLD 2277 Obsolete version of ~ sbal...
equs5av 2278 A property related to subs...
2sb5 2279 Equivalence for double sub...
sbco4lem 2280 Lemma for ~ sbco4 . It re...
sbco4 2281 Two ways of exchanging two...
dfsb7 2282 An alternate definition of...
sbn 2283 Negation inside and outsid...
sbex 2284 Move existential quantifie...
nf5 2285 Alternate definition of ~ ...
nf6 2286 An alternate definition of...
nf5d 2287 Deduce that ` x ` is not f...
nf5di 2288 Since the converse holds b...
19.9h 2289 A wff may be existentially...
19.21h 2290 Theorem 19.21 of [Margaris...
19.23h 2291 Theorem 19.23 of [Margaris...
exlimih 2292 Inference associated with ...
exlimdh 2293 Deduction form of Theorem ...
equsalhw 2294 Version of ~ equsalh with ...
equsexhv 2295 An equivalence related to ...
hba1 2296 The setvar ` x ` is not fr...
hbnt 2297 Closed theorem version of ...
hbn 2298 If ` x ` is not free in ` ...
hbnd 2299 Deduction form of bound-va...
hbim1 2300 A closed form of ~ hbim . ...
hbimd 2301 Deduction form of bound-va...
hbim 2302 If ` x ` is not free in ` ...
hban 2303 If ` x ` is not free in ` ...
hb3an 2304 If ` x ` is not free in ` ...
sbi2 2305 Introduction of implicatio...
sbim 2306 Implication inside and out...
sbrim 2307 Substitution in an implica...
sbrimv 2308 Substitution in an implica...
sblim 2309 Substitution in an implica...
sbor 2310 Disjunction inside and out...
sbbi 2311 Equivalence inside and out...
sblbis 2312 Introduce left bicondition...
sbrbis 2313 Introduce right biconditio...
sbrbif 2314 Introduce right biconditio...
sbiev 2315 Conversion of implicit sub...
sbiedw 2316 Conversion of implicit sub...
sbiedwOLD 2317 Obsolete version of ~ sbie...
axc7 2318 Show that the original axi...
axc7e 2319 Abbreviated version of ~ a...
modal-b 2320 The analogue in our predic...
19.9ht 2321 A closed version of ~ 19.9...
axc4 2322 Show that the original axi...
axc4i 2323 Inference version of ~ axc...
nfal 2324 If ` x ` is not free in ` ...
nfex 2325 If ` x ` is not free in ` ...
hbex 2326 If ` x ` is not free in ` ...
nfnf 2327 If ` x ` is not free in ` ...
19.12 2328 Theorem 19.12 of [Margaris...
nfald 2329 Deduction form of ~ nfal ....
nfexd 2330 If ` x ` is not free in ` ...
nfsbv 2331 If ` z ` is not free in ` ...
hbsbwOLD 2332 Obsolete version of ~ hbsb...
sbco2v 2333 A composition law for subs...
aaan 2334 Rearrange universal quanti...
eeor 2335 Rearrange existential quan...
cbv3v 2336 Rule used to change bound ...
cbv1v 2337 Rule used to change bound ...
cbv2w 2338 Rule used to change bound ...
cbvaldw 2339 Deduction used to change b...
cbvexdw 2340 Deduction used to change b...
cbv3hv 2341 Rule used to change bound ...
cbvalv1 2342 Rule used to change bound ...
cbvexv1 2343 Rule used to change bound ...
cbval2v 2344 Rule used to change bound ...
cbval2vOLD 2345 Obsolete version of ~ cbva...
cbvex2v 2346 Rule used to change bound ...
dvelimhw 2347 Proof of ~ dvelimh without...
pm11.53 2348 Theorem *11.53 in [Whitehe...
19.12vv 2349 Special case of ~ 19.12 wh...
eean 2350 Rearrange existential quan...
eeanv 2351 Distribute a pair of exist...
eeeanv 2352 Distribute three existenti...
ee4anv 2353 Distribute two pairs of ex...
sb8v 2354 Substitution of variable i...
sb8ev 2355 Substitution of variable i...
2sb8ev 2356 An equivalent expression f...
sb6rfv 2357 Reversed substitution. Ve...
sbnf2 2358 Two ways of expressing " `...
exsb 2359 An equivalent expression f...
2exsb 2360 An equivalent expression f...
sbbib 2361 Reversal of substitution. ...
sbbibvv 2362 Reversal of substitution. ...
cleljustALT 2363 Alternate proof of ~ clelj...
cleljustALT2 2364 Alternate proof of ~ clelj...
equs5aALT 2365 Alternate proof of ~ equs5...
equs5eALT 2366 Alternate proof of ~ equs5...
axc11r 2367 Same as ~ axc11 but with r...
dral1v 2368 Formula-building lemma for...
drex1v 2369 Formula-building lemma for...
drnf1v 2370 Formula-building lemma for...
ax13v 2372 A weaker version of ~ ax-1...
ax13lem1 2373 A version of ~ ax13v with ...
ax13 2374 Derive ~ ax-13 from ~ ax13...
ax13lem2 2375 Lemma for ~ nfeqf2 . This...
nfeqf2 2376 An equation between setvar...
dveeq2 2377 Quantifier introduction wh...
nfeqf1 2378 An equation between setvar...
dveeq1 2379 Quantifier introduction wh...
nfeqf 2380 A variable is effectively ...
axc9 2381 Derive set.mm's original ~...
ax6e 2382 At least one individual ex...
ax6 2383 Theorem showing that ~ ax-...
axc10 2384 Show that the original axi...
spimt 2385 Closed theorem form of ~ s...
spim 2386 Specialization, using impl...
spimed 2387 Deduction version of ~ spi...
spime 2388 Existential introduction, ...
spimv 2389 A version of ~ spim with a...
spimvALT 2390 Alternate proof of ~ spimv...
spimev 2391 Distinct-variable version ...
spv 2392 Specialization, using impl...
spei 2393 Inference from existential...
chvar 2394 Implicit substitution of `...
chvarv 2395 Implicit substitution of `...
cbv3 2396 Rule used to change bound ...
cbval 2397 Rule used to change bound ...
cbvex 2398 Rule used to change bound ...
cbvalv 2399 Rule used to change bound ...
cbvexv 2400 Rule used to change bound ...
cbv1 2401 Rule used to change bound ...
cbv2 2402 Rule used to change bound ...
cbv3h 2403 Rule used to change bound ...
cbv1h 2404 Rule used to change bound ...
cbv2h 2405 Rule used to change bound ...
cbvald 2406 Deduction used to change b...
cbvexd 2407 Deduction used to change b...
cbvaldva 2408 Rule used to change the bo...
cbvexdva 2409 Rule used to change the bo...
cbval2 2410 Rule used to change bound ...
cbvex2 2411 Rule used to change bound ...
cbval2vv 2412 Rule used to change bound ...
cbvex2vv 2413 Rule used to change bound ...
cbvex4v 2414 Rule used to change bound ...
equs4 2415 Lemma used in proofs of im...
equsal 2416 An equivalence related to ...
equsex 2417 An equivalence related to ...
equsexALT 2418 Alternate proof of ~ equse...
equsalh 2419 An equivalence related to ...
equsexh 2420 An equivalence related to ...
axc15 2421 Derivation of set.mm's ori...
ax12 2422 Rederivation of Axiom ~ ax...
ax12b 2423 A bidirectional version of...
ax13ALT 2424 Alternate proof of ~ ax13 ...
axc11n 2425 Derive set.mm's original ~...
aecom 2426 Commutation law for identi...
aecoms 2427 A commutation rule for ide...
naecoms 2428 A commutation rule for dis...
axc11 2429 Show that ~ ax-c11 can be ...
hbae 2430 All variables are effectiv...
hbnae 2431 All variables are effectiv...
nfae 2432 All variables are effectiv...
nfnae 2433 All variables are effectiv...
hbnaes 2434 Rule that applies ~ hbnae ...
axc16i 2435 Inference with ~ axc16 as ...
axc16nfALT 2436 Alternate proof of ~ axc16...
dral2 2437 Formula-building lemma for...
dral1 2438 Formula-building lemma for...
dral1ALT 2439 Alternate proof of ~ dral1...
drex1 2440 Formula-building lemma for...
drex2 2441 Formula-building lemma for...
drnf1 2442 Formula-building lemma for...
drnf2 2443 Formula-building lemma for...
nfald2 2444 Variation on ~ nfald which...
nfexd2 2445 Variation on ~ nfexd which...
exdistrf 2446 Distribution of existentia...
dvelimf 2447 Version of ~ dvelimv witho...
dvelimdf 2448 Deduction form of ~ dvelim...
dvelimh 2449 Version of ~ dvelim withou...
dvelim 2450 This theorem can be used t...
dvelimv 2451 Similar to ~ dvelim with f...
dvelimnf 2452 Version of ~ dvelim using ...
dveeq2ALT 2453 Alternate proof of ~ dveeq...
equvini 2454 A variable introduction la...
equvel 2455 A variable elimination law...
equs5a 2456 A property related to subs...
equs5e 2457 A property related to subs...
equs45f 2458 Two ways of expressing sub...
equs5 2459 Lemma used in proofs of su...
dveel1 2460 Quantifier introduction wh...
dveel2 2461 Quantifier introduction wh...
axc14 2462 Axiom ~ ax-c14 is redundan...
sb6x 2463 Equivalence involving subs...
sbequ5 2464 Substitution does not chan...
sbequ6 2465 Substitution does not chan...
sb5rf 2466 Reversed substitution. Us...
sb6rf 2467 Reversed substitution. Fo...
ax12vALT 2468 Alternate proof of ~ ax12v...
2ax6elem 2469 We can always find values ...
2ax6e 2470 We can always find values ...
2ax6eOLD 2471 Obsolete version of ~ 2ax6...
2sb5rf 2472 Reversed double substituti...
2sb6rf 2473 Reversed double substituti...
sbel2x 2474 Elimination of double subs...
sb4b 2475 Simplified definition of s...
sb4bOLD 2476 Obsolete version of ~ sb4b...
sb3b 2477 Simplified definition of s...
sb3 2478 One direction of a simplif...
sb1 2479 One direction of a simplif...
sb2 2480 One direction of a simplif...
sb3OLD 2481 Obsolete version of ~ sb3 ...
sb1OLD 2482 Obsolete version of ~ sb1 ...
sb3bOLD 2483 Obsolete version of ~ sb3b...
sb4a 2484 A version of one implicati...
dfsb1 2485 Alternate definition of su...
hbsb2 2486 Bound-variable hypothesis ...
nfsb2 2487 Bound-variable hypothesis ...
hbsb2a 2488 Special case of a bound-va...
sb4e 2489 One direction of a simplif...
hbsb2e 2490 Special case of a bound-va...
hbsb3 2491 If ` y ` is not free in ` ...
nfs1 2492 If ` y ` is not free in ` ...
axc16ALT 2493 Alternate proof of ~ axc16...
axc16gALT 2494 Alternate proof of ~ axc16...
equsb1 2495 Substitution applied to an...
equsb2 2496 Substitution applied to an...
dfsb2 2497 An alternate definition of...
dfsb3 2498 An alternate definition of...
drsb1 2499 Formula-building lemma for...
sb2ae 2500 In the case of two success...
sb6f 2501 Equivalence for substituti...
sb5f 2502 Equivalence for substituti...
nfsb4t 2503 A variable not free in a p...
nfsb4 2504 A variable not free in a p...
sbequ8 2505 Elimination of equality fr...
sbie 2506 Conversion of implicit sub...
sbied 2507 Conversion of implicit sub...
sbiedv 2508 Conversion of implicit sub...
2sbiev 2509 Conversion of double impli...
sbcom3 2510 Substituting ` y ` for ` x...
sbco 2511 A composition law for subs...
sbid2 2512 An identity law for substi...
sbid2v 2513 An identity law for substi...
sbidm 2514 An idempotent law for subs...
sbco2 2515 A composition law for subs...
sbco2d 2516 A composition law for subs...
sbco3 2517 A composition law for subs...
sbcom 2518 A commutativity law for su...
sbtrt 2519 Partially closed form of ~...
sbtr 2520 A partial converse to ~ sb...
sb8 2521 Substitution of variable i...
sb8e 2522 Substitution of variable i...
sb9 2523 Commutation of quantificat...
sb9i 2524 Commutation of quantificat...
sbhb 2525 Two ways of expressing " `...
nfsbd 2526 Deduction version of ~ nfs...
nfsb 2527 If ` z ` is not free in ` ...
nfsbOLD 2528 Obsolete version of ~ nfsb...
hbsb 2529 If ` z ` is not free in ` ...
sb7f 2530 This version of ~ dfsb7 do...
sb7h 2531 This version of ~ dfsb7 do...
sb10f 2532 Hao Wang's identity axiom ...
sbal1 2533 Check out ~ sbal for a ver...
sbal2 2534 Move quantifier in and out...
2sb8e 2535 An equivalent expression f...
dfmoeu 2536 An elementary proof of ~ m...
dfeumo 2537 An elementary proof showin...
mojust 2539 Soundness justification th...
nexmo 2541 Nonexistence implies uniqu...
exmo 2542 Any proposition holds for ...
moabs 2543 Absorption of existence co...
moim 2544 The at-most-one quantifier...
moimi 2545 The at-most-one quantifier...
moimdv 2546 The at-most-one quantifier...
mobi 2547 Equivalence theorem for th...
mobii 2548 Formula-building rule for ...
mobidv 2549 Formula-building rule for ...
mobid 2550 Formula-building rule for ...
moa1 2551 If an implication holds fo...
moan 2552 "At most one" is still the...
moani 2553 "At most one" is still tru...
moor 2554 "At most one" is still the...
mooran1 2555 "At most one" imports disj...
mooran2 2556 "At most one" exports disj...
nfmo1 2557 Bound-variable hypothesis ...
nfmod2 2558 Bound-variable hypothesis ...
nfmodv 2559 Bound-variable hypothesis ...
nfmov 2560 Bound-variable hypothesis ...
nfmod 2561 Bound-variable hypothesis ...
nfmo 2562 Bound-variable hypothesis ...
mof 2563 Version of ~ df-mo with di...
mo3 2564 Alternate definition of th...
mo 2565 Equivalent definitions of ...
mo4 2566 At-most-one quantifier exp...
mo4f 2567 At-most-one quantifier exp...
mo4OLD 2568 Obsolete version of ~ mo4 ...
eu3v 2571 An alternate way to expres...
eujust 2572 Soundness justification th...
eujustALT 2573 Alternate proof of ~ eujus...
eu6lem 2574 Lemma of ~ eu6im . A diss...
eu6 2575 Alternate definition of th...
eu6im 2576 One direction of ~ eu6 nee...
euf 2577 Version of ~ eu6 with disj...
euex 2578 Existential uniqueness imp...
eumo 2579 Existential uniqueness imp...
eumoi 2580 Uniqueness inferred from e...
exmoeub 2581 Existence implies that uni...
exmoeu 2582 Existence is equivalent to...
moeuex 2583 Uniqueness implies that ex...
moeu 2584 Uniqueness is equivalent t...
eubi 2585 Equivalence theorem for th...
eubii 2586 Introduce unique existenti...
eubidv 2587 Formula-building rule for ...
eubid 2588 Formula-building rule for ...
nfeu1 2589 Bound-variable hypothesis ...
nfeu1ALT 2590 Alternate proof of ~ nfeu1...
nfeud2 2591 Bound-variable hypothesis ...
nfeudw 2592 Bound-variable hypothesis ...
nfeud 2593 Bound-variable hypothesis ...
nfeuw 2594 Bound-variable hypothesis ...
nfeu 2595 Bound-variable hypothesis ...
dfeu 2596 Rederive ~ df-eu from the ...
dfmo 2597 Rederive ~ df-mo from the ...
euequ 2598 There exists a unique set ...
sb8eulem 2599 Lemma. Factor out the com...
sb8euv 2600 Variable substitution in u...
sb8eu 2601 Variable substitution in u...
sb8mo 2602 Variable substitution for ...
cbvmovw 2603 Change bound variable. Us...
cbvmow 2604 Rule used to change bound ...
cbvmowOLD 2605 Obsolete version of ~ cbvm...
cbvmo 2606 Rule used to change bound ...
cbveuvw 2607 Change bound variable. Us...
cbveuw 2608 Version of ~ cbveu with a ...
cbveuwOLD 2609 Obsolete version of ~ cbve...
cbveu 2610 Rule used to change bound ...
cbveuALT 2611 Alternative proof of ~ cbv...
eu2 2612 An alternate way of defini...
eu1 2613 An alternate way to expres...
euor 2614 Introduce a disjunct into ...
euorv 2615 Introduce a disjunct into ...
euor2 2616 Introduce or eliminate a d...
sbmo 2617 Substitution into an at-mo...
eu4 2618 Uniqueness using implicit ...
euimmo 2619 Existential uniqueness imp...
euim 2620 Add unique existential qua...
moanimlem 2621 Factor out the common proo...
moanimv 2622 Introduction of a conjunct...
moanim 2623 Introduction of a conjunct...
euan 2624 Introduction of a conjunct...
moanmo 2625 Nested at-most-one quantif...
moaneu 2626 Nested at-most-one and uni...
euanv 2627 Introduction of a conjunct...
mopick 2628 "At most one" picks a vari...
moexexlem 2629 Factor out the proof skele...
2moexv 2630 Double quantification with...
moexexvw 2631 "At most one" double quant...
2moswapv 2632 A condition allowing to sw...
2euswapv 2633 A condition allowing to sw...
2euexv 2634 Double quantification with...
2exeuv 2635 Double existential uniquen...
eupick 2636 Existential uniqueness "pi...
eupicka 2637 Version of ~ eupick with c...
eupickb 2638 Existential uniqueness "pi...
eupickbi 2639 Theorem *14.26 in [Whitehe...
mopick2 2640 "At most one" can show the...
moexex 2641 "At most one" double quant...
moexexv 2642 "At most one" double quant...
2moex 2643 Double quantification with...
2euex 2644 Double quantification with...
2eumo 2645 Nested unique existential ...
2eu2ex 2646 Double existential uniquen...
2moswap 2647 A condition allowing to sw...
2euswap 2648 A condition allowing to sw...
2exeu 2649 Double existential uniquen...
2mo2 2650 Two ways of expressing "th...
2mo 2651 Two ways of expressing "th...
2mos 2652 Double "there exists at mo...
2eu1 2653 Double existential uniquen...
2eu1v 2654 Double existential uniquen...
2eu2 2655 Double existential uniquen...
2eu3 2656 Double existential uniquen...
2eu4 2657 This theorem provides us w...
2eu5 2658 An alternate definition of...
2eu6 2659 Two equivalent expressions...
2eu7 2660 Two equivalent expressions...
2eu8 2661 Two equivalent expressions...
euae 2662 Two ways to express "exact...
exists1 2663 Two ways to express "exact...
exists2 2664 A condition implying that ...
barbara 2665 "Barbara", one of the fund...
celarent 2666 "Celarent", one of the syl...
darii 2667 "Darii", one of the syllog...
dariiALT 2668 Alternate proof of ~ darii...
ferio 2669 "Ferio" ("Ferioque"), one ...
barbarilem 2670 Lemma for ~ barbari and th...
barbari 2671 "Barbari", one of the syll...
barbariALT 2672 Alternate proof of ~ barba...
celaront 2673 "Celaront", one of the syl...
cesare 2674 "Cesare", one of the syllo...
camestres 2675 "Camestres", one of the sy...
festino 2676 "Festino", one of the syll...
festinoALT 2677 Alternate proof of ~ festi...
baroco 2678 "Baroco", one of the syllo...
barocoALT 2679 Alternate proof of ~ festi...
cesaro 2680 "Cesaro", one of the syllo...
camestros 2681 "Camestros", one of the sy...
datisi 2682 "Datisi", one of the syllo...
disamis 2683 "Disamis", one of the syll...
ferison 2684 "Ferison", one of the syll...
bocardo 2685 "Bocardo", one of the syll...
darapti 2686 "Darapti", one of the syll...
daraptiALT 2687 Alternate proof of ~ darap...
felapton 2688 "Felapton", one of the syl...
calemes 2689 "Calemes", one of the syll...
dimatis 2690 "Dimatis", one of the syll...
fresison 2691 "Fresison", one of the syl...
calemos 2692 "Calemos", one of the syll...
fesapo 2693 "Fesapo", one of the syllo...
bamalip 2694 "Bamalip", one of the syll...
axia1 2695 Left 'and' elimination (in...
axia2 2696 Right 'and' elimination (i...
axia3 2697 'And' introduction (intuit...
axin1 2698 'Not' introduction (intuit...
axin2 2699 'Not' elimination (intuiti...
axio 2700 Definition of 'or' (intuit...
axi4 2701 Specialization (intuitioni...
axi5r 2702 Converse of ~ axc4 (intuit...
axial 2703 The setvar ` x ` is not fr...
axie1 2704 The setvar ` x ` is not fr...
axie2 2705 A key property of existent...
axi9 2706 Axiom of existence (intuit...
axi10 2707 Axiom of Quantifier Substi...
axi12 2708 Axiom of Quantifier Introd...
axbnd 2709 Axiom of Bundling (intuiti...
axexte 2711 The axiom of extensionalit...
axextg 2712 A generalization of the ax...
axextb 2713 A bidirectional version of...
axextmo 2714 There exists at most one s...
nulmo 2715 There exists at most one e...
eleq1ab 2718 Extension (in the sense of...
cleljustab 2719 Extension of ~ cleljust fr...
abid 2720 Simplification of class ab...
vexwt 2721 A standard theorem of pred...
vexw 2722 If ` ph ` is a theorem, th...
vextru 2723 Every setvar is a member o...
hbab1 2724 Bound-variable hypothesis ...
nfsab1 2725 Bound-variable hypothesis ...
hbab 2726 Bound-variable hypothesis ...
hbabg 2727 Bound-variable hypothesis ...
nfsab 2728 Bound-variable hypothesis ...
nfsabg 2729 Bound-variable hypothesis ...
dfcleq 2731 The defining characterizat...
cvjust 2732 Every set is a class. Pro...
ax9ALT 2733 Proof of ~ ax-9 from Tarsk...
eleq2w2 2734 A weaker version of ~ eleq...
eqriv 2735 Infer equality of classes ...
eqrdv 2736 Deduce equality of classes...
eqrdav 2737 Deduce equality of classes...
eqid 2738 Law of identity (reflexivi...
eqidd 2739 Class identity law with an...
eqeq1d 2740 Deduction from equality to...
eqeq1dALT 2741 Shorter proof of ~ eqeq1d ...
eqeq1 2742 Equality implies equivalen...
eqeq1i 2743 Inference from equality to...
eqcomd 2744 Deduction from commutative...
eqcom 2745 Commutative law for class ...
eqcoms 2746 Inference applying commuta...
eqcomi 2747 Inference from commutative...
neqcomd 2748 Commute an inequality. (C...
eqeq2d 2749 Deduction from equality to...
eqeq2 2750 Equality implies equivalen...
eqeq2i 2751 Inference from equality to...
eqeq12 2752 Equality relationship amon...
eqeq12i 2753 A useful inference for sub...
eqeq12d 2754 A useful inference for sub...
eqeqan12d 2755 A useful inference for sub...
eqeqan12dALT 2756 Alternate proof of ~ eqeqa...
eqeqan12rd 2757 A useful inference for sub...
eqtr 2758 Transitive law for class e...
eqtr2 2759 A transitive law for class...
eqtr3 2760 A transitive law for class...
eqtri 2761 An equality transitivity i...
eqtr2i 2762 An equality transitivity i...
eqtr3i 2763 An equality transitivity i...
eqtr4i 2764 An equality transitivity i...
3eqtri 2765 An inference from three ch...
3eqtrri 2766 An inference from three ch...
3eqtr2i 2767 An inference from three ch...
3eqtr2ri 2768 An inference from three ch...
3eqtr3i 2769 An inference from three ch...
3eqtr3ri 2770 An inference from three ch...
3eqtr4i 2771 An inference from three ch...
3eqtr4ri 2772 An inference from three ch...
eqtrd 2773 An equality transitivity d...
eqtr2d 2774 An equality transitivity d...
eqtr3d 2775 An equality transitivity e...
eqtr4d 2776 An equality transitivity e...
3eqtrd 2777 A deduction from three cha...
3eqtrrd 2778 A deduction from three cha...
3eqtr2d 2779 A deduction from three cha...
3eqtr2rd 2780 A deduction from three cha...
3eqtr3d 2781 A deduction from three cha...
3eqtr3rd 2782 A deduction from three cha...
3eqtr4d 2783 A deduction from three cha...
3eqtr4rd 2784 A deduction from three cha...
syl5eq 2785 An equality transitivity d...
eqtr2id 2786 An equality transitivity d...
eqtr3id 2787 An equality transitivity d...
syl5reqr 2788 An equality transitivity d...
eqtrdi 2789 An equality transitivity d...
eqtr2di 2790 An equality transitivity d...
eqtr4di 2791 An equality transitivity d...
eqtr4id 2792 An equality transitivity d...
sylan9eq 2793 An equality transitivity d...
sylan9req 2794 An equality transitivity d...
sylan9eqr 2795 An equality transitivity d...
3eqtr3g 2796 A chained equality inferen...
3eqtr3a 2797 A chained equality inferen...
3eqtr4g 2798 A chained equality inferen...
3eqtr4a 2799 A chained equality inferen...
eq2tri 2800 A compound transitive infe...
abbi1 2801 Equivalent formulas yield ...
abbidv 2802 Equivalent wff's yield equ...
abbii 2803 Equivalent wff's yield equ...
abbid 2804 Equivalent wff's yield equ...
abbi 2805 Equivalent formulas define...
cbvabv 2806 Rule used to change bound ...
cbvabw 2807 Rule used to change bound ...
cbvabwOLD 2808 Obsolete version of ~ cbva...
cbvab 2809 Rule used to change bound ...
abeq2w 2810 Version of ~ abeq2 using i...
dfclel 2812 Characterization of the el...
elissetv 2813 An element of a class exis...
elisset 2814 An element of a class exis...
eleq1w 2815 Weaker version of ~ eleq1 ...
eleq2w 2816 Weaker version of ~ eleq2 ...
eleq1d 2817 Deduction from equality to...
eleq2d 2818 Deduction from equality to...
eleq2dALT 2819 Alternate proof of ~ eleq2...
eleq1 2820 Equality implies equivalen...
eleq2 2821 Equality implies equivalen...
eleq12 2822 Equality implies equivalen...
eleq1i 2823 Inference from equality to...
eleq2i 2824 Inference from equality to...
eleq12i 2825 Inference from equality to...
eqneltri 2826 If a class is not an eleme...
eleq12d 2827 Deduction from equality to...
eleq1a 2828 A transitive-type law rela...
eqeltri 2829 Substitution of equal clas...
eqeltrri 2830 Substitution of equal clas...
eleqtri 2831 Substitution of equal clas...
eleqtrri 2832 Substitution of equal clas...
eqeltrd 2833 Substitution of equal clas...
eqeltrrd 2834 Deduction that substitutes...
eleqtrd 2835 Deduction that substitutes...
eleqtrrd 2836 Deduction that substitutes...
eqeltrid 2837 A membership and equality ...
eqeltrrid 2838 A membership and equality ...
eleqtrid 2839 A membership and equality ...
eleqtrrid 2840 A membership and equality ...
eqeltrdi 2841 A membership and equality ...
eqeltrrdi 2842 A membership and equality ...
eleqtrdi 2843 A membership and equality ...
eleqtrrdi 2844 A membership and equality ...
3eltr3i 2845 Substitution of equal clas...
3eltr4i 2846 Substitution of equal clas...
3eltr3d 2847 Substitution of equal clas...
3eltr4d 2848 Substitution of equal clas...
3eltr3g 2849 Substitution of equal clas...
3eltr4g 2850 Substitution of equal clas...
eleq2s 2851 Substitution of equal clas...
eqneltrd 2852 If a class is not an eleme...
eqneltrrd 2853 If a class is not an eleme...
neleqtrd 2854 If a class is not an eleme...
neleqtrrd 2855 If a class is not an eleme...
cleqh 2856 Establish equality between...
nelneq 2857 A way of showing two class...
nelneq2 2858 A way of showing two class...
eqsb3 2859 Substitution applied to an...
clelsb3 2860 Substitution applied to an...
hbxfreq 2861 A utility lemma to transfe...
hblem 2862 Change the free variable o...
hblemg 2863 Change the free variable o...
abeq2 2864 Equality of a class variab...
abeq1 2865 Equality of a class variab...
abeq2d 2866 Equality of a class variab...
abeq2i 2867 Equality of a class variab...
abeq1i 2868 Equality of a class variab...
abbi2dv 2869 Deduction from a wff to a ...
abbi1dv 2870 Deduction from a wff to a ...
abbi2i 2871 Equality of a class variab...
abbiOLD 2872 Obsolete proof of ~ abbi a...
abid1 2873 Every class is equal to a ...
abid2 2874 A simplification of class ...
clelab 2875 Membership of a class vari...
clelabOLD 2876 Obsolete version of ~ clel...
clabel 2877 Membership of a class abst...
sbab 2878 The right-hand side of the...
nfcjust 2880 Justification theorem for ...
nfci 2882 Deduce that a class ` A ` ...
nfcii 2883 Deduce that a class ` A ` ...
nfcr 2884 Consequence of the not-fre...
nfcrALT 2885 Alternate version of ~ nfc...
nfcri 2886 Consequence of the not-fre...
nfcd 2887 Deduce that a class ` A ` ...
nfcrd 2888 Consequence of the not-fre...
nfcriOLD 2889 Obsolete version of ~ nfcr...
nfcriOLDOLD 2890 Obsolete version of ~ nfcr...
nfcrii 2891 Consequence of the not-fre...
nfcriiOLD 2892 Obsolete version of ~ nfcr...
nfcriOLDOLDOLD 2893 Obsolete version of ~ nfcr...
nfceqdf 2894 An equality theorem for ef...
nfceqdfOLD 2895 Obsolete version of ~ nfce...
nfceqi 2896 Equality theorem for class...
nfcxfr 2897 A utility lemma to transfe...
nfcxfrd 2898 A utility lemma to transfe...
nfcv 2899 If ` x ` is disjoint from ...
nfcvd 2900 If ` x ` is disjoint from ...
nfab1 2901 Bound-variable hypothesis ...
nfnfc1 2902 The setvar ` x ` is bound ...
clelsb3fw 2903 Substitution applied to an...
clelsb3f 2904 Substitution applied to an...
nfab 2905 Bound-variable hypothesis ...
nfabg 2906 Bound-variable hypothesis ...
nfaba1 2907 Bound-variable hypothesis ...
nfaba1g 2908 Bound-variable hypothesis ...
nfeqd 2909 Hypothesis builder for equ...
nfeld 2910 Hypothesis builder for ele...
nfnfc 2911 Hypothesis builder for ` F...
nfeq 2912 Hypothesis builder for equ...
nfel 2913 Hypothesis builder for ele...
nfeq1 2914 Hypothesis builder for equ...
nfel1 2915 Hypothesis builder for ele...
nfeq2 2916 Hypothesis builder for equ...
nfel2 2917 Hypothesis builder for ele...
drnfc1 2918 Formula-building lemma for...
drnfc1OLD 2919 Obsolete version of ~ drnf...
drnfc2 2920 Formula-building lemma for...
drnfc2OLD 2921 Obsolete version of ~ drnf...
nfabdw 2922 Bound-variable hypothesis ...
nfabdwOLD 2923 Obsolete version of ~ nfab...
nfabd 2924 Bound-variable hypothesis ...
nfabd2 2925 Bound-variable hypothesis ...
dvelimdc 2926 Deduction form of ~ dvelim...
dvelimc 2927 Version of ~ dvelim for cl...
nfcvf 2928 If ` x ` and ` y ` are dis...
nfcvf2 2929 If ` x ` and ` y ` are dis...
cleqf 2930 Establish equality between...
abid2f 2931 A simplification of class ...
abeq2f 2932 Equality of a class variab...
sbabel 2933 Theorem to move a substitu...
neii 2936 Inference associated with ...
neir 2937 Inference associated with ...
nne 2938 Negation of inequality. (...
neneqd 2939 Deduction eliminating ineq...
neneq 2940 From inequality to non-equ...
neqned 2941 If it is not the case that...
neqne 2942 From non-equality to inequ...
neirr 2943 No class is unequal to its...
exmidne 2944 Excluded middle with equal...
eqneqall 2945 A contradiction concerning...
nonconne 2946 Law of noncontradiction wi...
necon3ad 2947 Contrapositive law deducti...
necon3bd 2948 Contrapositive law deducti...
necon2ad 2949 Contrapositive inference f...
necon2bd 2950 Contrapositive inference f...
necon1ad 2951 Contrapositive deduction f...
necon1bd 2952 Contrapositive deduction f...
necon4ad 2953 Contrapositive inference f...
necon4bd 2954 Contrapositive inference f...
necon3d 2955 Contrapositive law deducti...
necon1d 2956 Contrapositive law deducti...
necon2d 2957 Contrapositive inference f...
necon4d 2958 Contrapositive inference f...
necon3ai 2959 Contrapositive inference f...
necon3bi 2960 Contrapositive inference f...
necon1ai 2961 Contrapositive inference f...
necon1bi 2962 Contrapositive inference f...
necon2ai 2963 Contrapositive inference f...
necon2bi 2964 Contrapositive inference f...
necon4ai 2965 Contrapositive inference f...
necon3i 2966 Contrapositive inference f...
necon1i 2967 Contrapositive inference f...
necon2i 2968 Contrapositive inference f...
necon4i 2969 Contrapositive inference f...
necon3abid 2970 Deduction from equality to...
necon3bbid 2971 Deduction from equality to...
necon1abid 2972 Contrapositive deduction f...
necon1bbid 2973 Contrapositive inference f...
necon4abid 2974 Contrapositive law deducti...
necon4bbid 2975 Contrapositive law deducti...
necon2abid 2976 Contrapositive deduction f...
necon2bbid 2977 Contrapositive deduction f...
necon3bid 2978 Deduction from equality to...
necon4bid 2979 Contrapositive law deducti...
necon3abii 2980 Deduction from equality to...
necon3bbii 2981 Deduction from equality to...
necon1abii 2982 Contrapositive inference f...
necon1bbii 2983 Contrapositive inference f...
necon2abii 2984 Contrapositive inference f...
necon2bbii 2985 Contrapositive inference f...
necon3bii 2986 Inference from equality to...
necom 2987 Commutation of inequality....
necomi 2988 Inference from commutative...
necomd 2989 Deduction from commutative...
nesym 2990 Characterization of inequa...
nesymi 2991 Inference associated with ...
nesymir 2992 Inference associated with ...
neeq1d 2993 Deduction for inequality. ...
neeq2d 2994 Deduction for inequality. ...
neeq12d 2995 Deduction for inequality. ...
neeq1 2996 Equality theorem for inequ...
neeq2 2997 Equality theorem for inequ...
neeq1i 2998 Inference for inequality. ...
neeq2i 2999 Inference for inequality. ...
neeq12i 3000 Inference for inequality. ...
eqnetrd 3001 Substitution of equal clas...
eqnetrrd 3002 Substitution of equal clas...
neeqtrd 3003 Substitution of equal clas...
eqnetri 3004 Substitution of equal clas...
eqnetrri 3005 Substitution of equal clas...
neeqtri 3006 Substitution of equal clas...
neeqtrri 3007 Substitution of equal clas...
neeqtrrd 3008 Substitution of equal clas...
eqnetrrid 3009 A chained equality inferen...
3netr3d 3010 Substitution of equality i...
3netr4d 3011 Substitution of equality i...
3netr3g 3012 Substitution of equality i...
3netr4g 3013 Substitution of equality i...
nebi 3014 Contraposition law for ine...
pm13.18 3015 Theorem *13.18 in [Whitehe...
pm13.181 3016 Theorem *13.181 in [Whiteh...
pm2.61ine 3017 Inference eliminating an i...
pm2.21ddne 3018 A contradiction implies an...
pm2.61ne 3019 Deduction eliminating an i...
pm2.61dne 3020 Deduction eliminating an i...
pm2.61dane 3021 Deduction eliminating an i...
pm2.61da2ne 3022 Deduction eliminating two ...
pm2.61da3ne 3023 Deduction eliminating thre...
pm2.61iine 3024 Equality version of ~ pm2....
neor 3025 Logical OR with an equalit...
neanior 3026 A De Morgan's law for ineq...
ne3anior 3027 A De Morgan's law for ineq...
neorian 3028 A De Morgan's law for ineq...
nemtbir 3029 An inference from an inequ...
nelne1 3030 Two classes are different ...
nelne2 3031 Two classes are different ...
nelelne 3032 Two classes are different ...
neneor 3033 If two classes are differe...
nfne 3034 Bound-variable hypothesis ...
nfned 3035 Bound-variable hypothesis ...
nabbi 3036 Not equivalent wff's corre...
mteqand 3037 A modus tollens deduction ...
neli 3040 Inference associated with ...
nelir 3041 Inference associated with ...
neleq12d 3042 Equality theorem for negat...
neleq1 3043 Equality theorem for negat...
neleq2 3044 Equality theorem for negat...
nfnel 3045 Bound-variable hypothesis ...
nfneld 3046 Bound-variable hypothesis ...
nnel 3047 Negation of negated member...
elnelne1 3048 Two classes are different ...
elnelne2 3049 Two classes are different ...
nelcon3d 3050 Contrapositive law deducti...
elnelall 3051 A contradiction concerning...
pm2.61danel 3052 Deduction eliminating an e...
rgen 3063 Generalization rule for re...
ralel 3064 All elements of a class ar...
rgenw 3065 Generalization rule for re...
rgen2w 3066 Generalization rule for re...
mprg 3067 Modus ponens combined with...
mprgbir 3068 Modus ponens on biconditio...
alral 3069 Universal quantification i...
raln 3070 Restricted universally qua...
ral2imi 3071 Inference quantifying ante...
ralimi2 3072 Inference quantifying both...
ralimia 3073 Inference quantifying both...
ralimiaa 3074 Inference quantifying both...
ralimi 3075 Inference quantifying both...
2ralimi 3076 Inference quantifying both...
ralim 3077 Distribution of restricted...
ralbii2 3078 Inference adding different...
ralbiia 3079 Inference adding restricte...
ralbii 3080 Inference adding restricte...
2ralbii 3081 Inference adding two restr...
ralbi 3082 Distribute a restricted un...
ralanid 3083 Cancellation law for restr...
r19.26 3084 Restricted quantifier vers...
r19.26-2 3085 Restricted quantifier vers...
r19.26-3 3086 Version of ~ r19.26 with t...
r19.26m 3087 Version of ~ 19.26 and ~ r...
ralbiim 3088 Split a biconditional and ...
r19.21v 3089 Restricted quantifier vers...
ralimdv2 3090 Inference quantifying both...
ralimdva 3091 Deduction quantifying both...
ralimdv 3092 Deduction quantifying both...
ralimdvva 3093 Deduction doubly quantifyi...
hbralrimi 3094 Inference from Theorem 19....
ralrimiv 3095 Inference from Theorem 19....
ralrimiva 3096 Inference from Theorem 19....
ralrimivw 3097 Inference from Theorem 19....
r19.27v 3098 Restricted quantitifer ver...
r19.28v 3099 Restricted quantifier vers...
ralrimdv 3100 Inference from Theorem 19....
ralrimdva 3101 Inference from Theorem 19....
ralrimivv 3102 Inference from Theorem 19....
ralrimivva 3103 Inference from Theorem 19....
ralrimivvva 3104 Inference from Theorem 19....
ralrimdvv 3105 Inference from Theorem 19....
ralrimdvva 3106 Inference from Theorem 19....
ralbidv2 3107 Formula-building rule for ...
ralbidva 3108 Formula-building rule for ...
ralbidv 3109 Formula-building rule for ...
2ralbidva 3110 Formula-building rule for ...
2ralbidv 3111 Formula-building rule for ...
r2allem 3112 Lemma factoring out common...
r2al 3113 Double restricted universa...
r3al 3114 Triple restricted universa...
rgen2 3115 Generalization rule for re...
rgen3 3116 Generalization rule for re...
rsp 3117 Restricted specialization....
rspa 3118 Restricted specialization....
rspec 3119 Specialization rule for re...
r19.21bi 3120 Inference from Theorem 19....
r19.21be 3121 Inference from Theorem 19....
rspec2 3122 Specialization rule for re...
rspec3 3123 Specialization rule for re...
rsp2 3124 Restricted specialization,...
r19.21t 3125 Restricted quantifier vers...
r19.21 3126 Restricted quantifier vers...
ralrimi 3127 Inference from Theorem 19....
ralimdaa 3128 Deduction quantifying both...
ralrimd 3129 Inference from Theorem 19....
nfra1 3130 The setvar ` x ` is not fr...
hbra1 3131 The setvar ` x ` is not fr...
hbral 3132 Bound-variable hypothesis ...
r2alf 3133 Double restricted universa...
nfraldw 3134 Deduction version of ~ nfr...
nfraldwOLD 3135 Obsolete version of ~ nfra...
nfrald 3136 Deduction version of ~ nfr...
nfralw 3137 Bound-variable hypothesis ...
nfral 3138 Bound-variable hypothesis ...
nfra2w 3139 Similar to Lemma 24 of [Mo...
nfra2wOLD 3140 Obsolete version of ~ nfra...
nfra2 3141 Similar to Lemma 24 of [Mo...
rgen2a 3142 Generalization rule for re...
ralbida 3143 Formula-building rule for ...
ralbid 3144 Formula-building rule for ...
2ralbida 3145 Formula-building rule for ...
raleqbii 3146 Equality deduction for res...
ralcom4 3147 Commutation of restricted ...
ralnex 3148 Relationship between restr...
dfral2 3149 Relationship between restr...
rexnal 3150 Relationship between restr...
dfrex2 3151 Relationship between restr...
rexex 3152 Restricted existence impli...
rexim 3153 Theorem 19.22 of [Margaris...
rexbi 3154 Distribute restricted quan...
reximia 3155 Inference quantifying both...
reximi 3156 Inference quantifying both...
reximi2 3157 Inference quantifying both...
rexbii2 3158 Inference adding different...
rexbiia 3159 Inference adding restricte...
rexbii 3160 Inference adding restricte...
2rexbii 3161 Inference adding two restr...
rexcom4 3162 Commutation of restricted ...
2ex2rexrot 3163 Rotate two existential qua...
rexcom4a 3164 Specialized existential co...
rexanid 3165 Cancellation law for restr...
r19.29 3166 Restricted quantifier vers...
r19.29r 3167 Restricted quantifier vers...
r19.29imd 3168 Theorem 19.29 of [Margaris...
rexnal2 3169 Relationship between two r...
rexnal3 3170 Relationship between three...
ralnex2 3171 Relationship between two r...
ralnex3 3172 Relationship between three...
ralinexa 3173 A transformation of restri...
rexanali 3174 A transformation of restri...
nrexralim 3175 Negation of a complex pred...
risset 3176 Two ways to say " ` A ` be...
nelb 3177 A definition of ` -. A e. ...
nrex 3178 Inference adding restricte...
nrexdv 3179 Deduction adding restricte...
reximdv2 3180 Deduction quantifying both...
reximdvai 3181 Deduction quantifying both...
reximdv 3182 Deduction from Theorem 19....
reximdva 3183 Deduction quantifying both...
reximddv 3184 Deduction from Theorem 19....
reximssdv 3185 Derivation of a restricted...
reximdvva 3186 Deduction doubly quantifyi...
reximddv2 3187 Double deduction from Theo...
r19.23v 3188 Restricted quantifier vers...
rexlimiv 3189 Inference from Theorem 19....
rexlimiva 3190 Inference from Theorem 19....
rexlimivw 3191 Weaker version of ~ rexlim...
rexlimdv 3192 Inference from Theorem 19....
rexlimdva 3193 Inference from Theorem 19....
rexlimdvaa 3194 Inference from Theorem 19....
rexlimdv3a 3195 Inference from Theorem 19....
rexlimdva2 3196 Inference from Theorem 19....
r19.29an 3197 A commonly used pattern in...
r19.29a 3198 A commonly used pattern in...
rexlimdvw 3199 Inference from Theorem 19....
rexlimddv 3200 Restricted existential eli...
rexlimivv 3201 Inference from Theorem 19....
rexlimdvv 3202 Inference from Theorem 19....
rexlimdvva 3203 Inference from Theorem 19....
rexbidv2 3204 Formula-building rule for ...
rexbidva 3205 Formula-building rule for ...
rexbidv 3206 Formula-building rule for ...
2rexbiia 3207 Inference adding two restr...
2rexbidva 3208 Formula-building rule for ...
2rexbidv 3209 Formula-building rule for ...
rexralbidv 3210 Formula-building rule for ...
r2exlem 3211 Lemma factoring out common...
r2ex 3212 Double restricted existent...
rspe 3213 Restricted specialization....
rsp2e 3214 Restricted specialization....
nfre1 3215 The setvar ` x ` is not fr...
nfrexd 3216 Deduction version of ~ nfr...
nfrexdg 3217 Deduction version of ~ nfr...
nfrex 3218 Bound-variable hypothesis ...
nfrexg 3219 Bound-variable hypothesis ...
reximdai 3220 Deduction from Theorem 19....
reximd2a 3221 Deduction quantifying both...
r19.23t 3222 Closed theorem form of ~ r...
r19.23 3223 Restricted quantifier vers...
rexlimi 3224 Restricted quantifier vers...
rexlimd2 3225 Version of ~ rexlimd with ...
rexlimd 3226 Deduction form of ~ rexlim...
rexbida 3227 Formula-building rule for ...
rexbidvaALT 3228 Alternate proof of ~ rexbi...
rexbid 3229 Formula-building rule for ...
rexbidvALT 3230 Alternate proof of ~ rexbi...
ralrexbid 3231 Formula-building rule for ...
ralrexbidOLD 3232 Obsolete version of ~ ralr...
r19.12 3233 Restricted quantifier vers...
r2exf 3234 Double restricted existent...
rexeqbii 3235 Equality deduction for res...
reuanid 3236 Cancellation law for restr...
rmoanid 3237 Cancellation law for restr...
r19.29af2 3238 A commonly used pattern ba...
r19.29af 3239 A commonly used pattern ba...
2r19.29 3240 Theorem ~ r19.29 with two ...
r19.29d2r 3241 Theorem 19.29 of [Margaris...
r19.29vva 3242 A commonly used pattern ba...
r19.30 3243 Restricted quantifier vers...
r19.32v 3244 Restricted quantifier vers...
r19.35 3245 Restricted quantifier vers...
r19.36v 3246 Restricted quantifier vers...
r19.37 3247 Restricted quantifier vers...
r19.37v 3248 Restricted quantifier vers...
r19.40 3249 Restricted quantifier vers...
r19.41v 3250 Restricted quantifier vers...
r19.41 3251 Restricted quantifier vers...
r19.41vv 3252 Version of ~ r19.41v with ...
r19.42v 3253 Restricted quantifier vers...
r19.43 3254 Restricted quantifier vers...
r19.44v 3255 One direction of a restric...
r19.45v 3256 Restricted quantifier vers...
ralcom 3257 Commutation of restricted ...
rexcom 3258 Commutation of restricted ...
ralcomf 3259 Commutation of restricted ...
rexcomf 3260 Commutation of restricted ...
ralcom13 3261 Swap first and third restr...
rexcom13 3262 Swap first and third restr...
ralrot3 3263 Rotate three restricted un...
rexrot4 3264 Rotate four restricted exi...
ralcom2 3265 Commutation of restricted ...
ralcom3 3266 A commutation law for rest...
reeanlem 3267 Lemma factoring out common...
reean 3268 Rearrange restricted exist...
reeanv 3269 Rearrange restricted exist...
3reeanv 3270 Rearrange three restricted...
2ralor 3271 Distribute restricted univ...
nfreu1 3272 The setvar ` x ` is not fr...
nfrmo1 3273 The setvar ` x ` is not fr...
nfreud 3274 Deduction version of ~ nfr...
nfrmod 3275 Deduction version of ~ nfr...
nfreuw 3276 Bound-variable hypothesis ...
nfrmow 3277 Bound-variable hypothesis ...
nfreu 3278 Bound-variable hypothesis ...
nfrmo 3279 Bound-variable hypothesis ...
rabid 3280 An "identity" law of concr...
rabrab 3281 Abstract builder restricte...
rabidim1 3282 Membership in a restricted...
rabid2 3283 An "identity" law for rest...
rabid2f 3284 An "identity" law for rest...
rabbi 3285 Equivalent wff's correspon...
nfrab1 3286 The abstraction variable i...
nfrabw 3287 A variable not free in a w...
nfrab 3288 A variable not free in a w...
reubida 3289 Formula-building rule for ...
reubidva 3290 Formula-building rule for ...
reubidv 3291 Formula-building rule for ...
reubiia 3292 Formula-building rule for ...
reubii 3293 Formula-building rule for ...
rmobida 3294 Formula-building rule for ...
rmobidva 3295 Formula-building rule for ...
rmobidv 3296 Formula-building rule for ...
rmobiia 3297 Formula-building rule for ...
rmobii 3298 Formula-building rule for ...
raleqf 3299 Equality theorem for restr...
rexeqf 3300 Equality theorem for restr...
reueq1f 3301 Equality theorem for restr...
rmoeq1f 3302 Equality theorem for restr...
raleqbidv 3303 Equality deduction for res...
rexeqbidv 3304 Equality deduction for res...
raleqbidvv 3305 Version of ~ raleqbidv wit...
rexeqbidvv 3306 Version of ~ rexeqbidv wit...
raleqbi1dv 3307 Equality deduction for res...
rexeqbi1dv 3308 Equality deduction for res...
raleq 3309 Equality theorem for restr...
rexeq 3310 Equality theorem for restr...
reueq1 3311 Equality theorem for restr...
rmoeq1 3312 Equality theorem for restr...
raleqi 3313 Equality inference for res...
rexeqi 3314 Equality inference for res...
raleqdv 3315 Equality deduction for res...
rexeqdv 3316 Equality deduction for res...
reueqd 3317 Equality deduction for res...
rmoeqd 3318 Equality deduction for res...
raleqbid 3319 Equality deduction for res...
rexeqbid 3320 Equality deduction for res...
raleqbidva 3321 Equality deduction for res...
rexeqbidva 3322 Equality deduction for res...
raleleq 3323 All elements of a class ar...
raleleqALT 3324 Alternate proof of ~ ralel...
moel 3325 "At most one" element in a...
mormo 3326 Unrestricted "at most one"...
reu5 3327 Restricted uniqueness in t...
reurex 3328 Restricted unique existenc...
2reu2rex 3329 Double restricted existent...
reurmo 3330 Restricted existential uni...
rmo5 3331 Restricted "at most one" i...
nrexrmo 3332 Nonexistence implies restr...
reueubd 3333 Restricted existential uni...
cbvralfw 3334 Rule used to change bound ...
cbvralfwOLD 3335 Obsolete version of ~ cbvr...
cbvrexfw 3336 Rule used to change bound ...
cbvralf 3337 Rule used to change bound ...
cbvrexf 3338 Rule used to change bound ...
cbvralw 3339 Rule used to change bound ...
cbvrexw 3340 Rule used to change bound ...
cbvreuw 3341 Change the bound variable ...
cbvrmow 3342 Change the bound variable ...
cbvrmowOLD 3343 Obsolete version of ~ cbvr...
cbvral 3344 Rule used to change bound ...
cbvrex 3345 Rule used to change bound ...
cbvreu 3346 Change the bound variable ...
cbvrmo 3347 Change the bound variable ...
cbvralvw 3348 Change the bound variable ...
cbvrexvw 3349 Change the bound variable ...
cbvrmovw 3350 Change the bound variable ...
cbvreuvw 3351 Change the bound variable ...
cbvreuvwOLD 3352 Obsolete version of ~ cbvr...
cbvralv 3353 Change the bound variable ...
cbvrexv 3354 Change the bound variable ...
cbvreuv 3355 Change the bound variable ...
cbvrmov 3356 Change the bound variable ...
cbvraldva2 3357 Rule used to change the bo...
cbvrexdva2 3358 Rule used to change the bo...
cbvraldva 3359 Rule used to change the bo...
cbvrexdva 3360 Rule used to change the bo...
cbvral2vw 3361 Change bound variables of ...
cbvrex2vw 3362 Change bound variables of ...
cbvral3vw 3363 Change bound variables of ...
cbvral2v 3364 Change bound variables of ...
cbvrex2v 3365 Change bound variables of ...
cbvral3v 3366 Change bound variables of ...
cbvralsvw 3367 Change bound variable by u...
cbvrexsvw 3368 Change bound variable by u...
cbvralsv 3369 Change bound variable by u...
cbvrexsv 3370 Change bound variable by u...
sbralie 3371 Implicit to explicit subst...
rabbiia 3372 Equivalent formulas yield ...
rabbii 3373 Equivalent wff's correspon...
rabbida 3374 Equivalent wff's yield equ...
rabbid 3375 Version of ~ rabbidv with ...
rabbidva2 3376 Equivalent wff's yield equ...
rabbia2 3377 Equivalent wff's yield equ...
rabbidva 3378 Equivalent wff's yield equ...
rabbidvaOLD 3379 Obsolete proof of ~ rabbid...
rabbidv 3380 Equivalent wff's yield equ...
rabeqf 3381 Equality theorem for restr...
rabeqi 3382 Equality theorem for restr...
rabeqiOLD 3383 Obsolete version of ~ rabe...
rabeq 3384 Equality theorem for restr...
rabeqdv 3385 Equality of restricted cla...
rabeqbidv 3386 Equality of restricted cla...
rabeqbidva 3387 Equality of restricted cla...
rabeq2i 3388 Inference from equality of...
rabswap 3389 Swap with a membership rel...
cbvrabw 3390 Rule to change the bound v...
cbvrab 3391 Rule to change the bound v...
cbvrabv 3392 Rule to change the bound v...
rabrabi 3393 Abstract builder restricte...
rabeqcda 3394 When ` ps ` is always true...
ralrimia 3395 Inference from Theorem 19....
ralimda 3396 Deduction quantifying both...
vjust 3398 Justification theorem for ...
dfv2 3400 Alternate definition of th...
vex 3401 All setvar variables are s...
vexOLD 3402 Obsolete version of ~ vex ...
elv 3403 If a proposition is implie...
elvd 3404 If a proposition is implie...
el2v 3405 If a proposition is implie...
eqv 3406 The universe contains ever...
eqvf 3407 The universe contains ever...
abv 3408 The class of sets verifyin...
abvALT 3409 Alternate proof of ~ abv ,...
isset 3410 Two ways to express that "...
issetf 3411 A version of ~ isset that ...
isseti 3412 A way to say " ` A ` is a ...
issetri 3413 A way to say " ` A ` is a ...
eqvisset 3414 A class equal to a variabl...
elex 3415 If a class is a member of ...
elexi 3416 If a class is a member of ...
elexd 3417 If a class is a member of ...
elex2 3418 If a class contains anothe...
elex22 3419 If two classes each contai...
prcnel 3420 A proper class doesn't bel...
ralv 3421 A universal quantifier res...
rexv 3422 An existential quantifier ...
reuv 3423 A unique existential quant...
rmov 3424 An at-most-one quantifier ...
rabab 3425 A class abstraction restri...
rexcom4b 3426 Specialized existential co...
ceqsalt 3427 Closed theorem version of ...
ceqsralt 3428 Restricted quantifier vers...
ceqsalg 3429 A representation of explic...
ceqsalgALT 3430 Alternate proof of ~ ceqsa...
ceqsal 3431 A representation of explic...
ceqsalv 3432 A representation of explic...
ceqsalvOLD 3433 Obsolete version of ~ ceqs...
ceqsralv 3434 Restricted quantifier vers...
ceqsralvOLD 3435 Obsolete version of ~ ceqs...
gencl 3436 Implicit substitution for ...
2gencl 3437 Implicit substitution for ...
3gencl 3438 Implicit substitution for ...
cgsexg 3439 Implicit substitution infe...
cgsex2g 3440 Implicit substitution infe...
cgsex4g 3441 An implicit substitution i...
cgsex4gOLD 3442 Obsolete version of ~ cgse...
ceqsex 3443 Elimination of an existent...
ceqsexv 3444 Elimination of an existent...
ceqsexv2d 3445 Elimination of an existent...
ceqsex2 3446 Elimination of two existen...
ceqsex2v 3447 Elimination of two existen...
ceqsex3v 3448 Elimination of three exist...
ceqsex4v 3449 Elimination of four existe...
ceqsex6v 3450 Elimination of six existen...
ceqsex8v 3451 Elimination of eight exist...
gencbvex 3452 Change of bound variable u...
gencbvex2 3453 Restatement of ~ gencbvex ...
gencbval 3454 Change of bound variable u...
sbhypf 3455 Introduce an explicit subs...
vtoclgft 3456 Closed theorem form of ~ v...
vtoclgftOLD 3457 Obsolete version of ~ vtoc...
vtocldf 3458 Implicit substitution of a...
vtocld 3459 Implicit substitution of a...
vtocldOLD 3460 Obsolete version of ~ vtoc...
vtocl2d 3461 Implicit substitution of t...
vtoclf 3462 Implicit substitution of a...
vtocl 3463 Implicit substitution of a...
vtoclALT 3464 Alternate proof of ~ vtocl...
vtocl2 3465 Implicit substitution of c...
vtocl3 3466 Implicit substitution of c...
vtoclb 3467 Implicit substitution of a...
vtoclgf 3468 Implicit substitution of a...
vtoclg1f 3469 Version of ~ vtoclgf with ...
vtoclg 3470 Implicit substitution of a...
vtoclgOLD 3471 Obsolete version of ~ vtoc...
vtoclbg 3472 Implicit substitution of a...
vtocl2gf 3473 Implicit substitution of a...
vtocl3gf 3474 Implicit substitution of a...
vtocl2g 3475 Implicit substitution of 2...
vtoclgaf 3476 Implicit substitution of a...
vtoclga 3477 Implicit substitution of a...
vtocl2ga 3478 Implicit substitution of 2...
vtocl2gaf 3479 Implicit substitution of 2...
vtocl3gaf 3480 Implicit substitution of 3...
vtocl3ga 3481 Implicit substitution of 3...
vtocl4g 3482 Implicit substitution of 4...
vtocl4ga 3483 Implicit substitution of 4...
vtocleg 3484 Implicit substitution of a...
vtoclegft 3485 Implicit substitution of a...
vtoclef 3486 Implicit substitution of a...
vtocle 3487 Implicit substitution of a...
vtoclri 3488 Implicit substitution of a...
spcimgft 3489 A closed version of ~ spci...
spcgft 3490 A closed version of ~ spcg...
spcimgf 3491 Rule of specialization, us...
spcimegf 3492 Existential specialization...
spcgf 3493 Rule of specialization, us...
spcegf 3494 Existential specialization...
spcimdv 3495 Restricted specialization,...
spcdv 3496 Rule of specialization, us...
spcimedv 3497 Restricted existential spe...
spcgv 3498 Rule of specialization, us...
spcegv 3499 Existential specialization...
spcedv 3500 Existential specialization...
spc2egv 3501 Existential specialization...
spc2gv 3502 Specialization with two qu...
spc2ed 3503 Existential specialization...
spc2d 3504 Specialization with 2 quan...
spc3egv 3505 Existential specialization...
spc3gv 3506 Specialization with three ...
spcv 3507 Rule of specialization, us...
spcev 3508 Existential specialization...
spc2ev 3509 Existential specialization...
rspct 3510 A closed version of ~ rspc...
rspcdf 3511 Restricted specialization,...
rspc 3512 Restricted specialization,...
rspce 3513 Restricted existential spe...
rspcimdv 3514 Restricted specialization,...
rspcimedv 3515 Restricted existential spe...
rspcdv 3516 Restricted specialization,...
rspcedv 3517 Restricted existential spe...
rspcebdv 3518 Restricted existential spe...
rspcv 3519 Restricted specialization,...
rspcvOLD 3520 Obsolete version of ~ rspc...
rspccv 3521 Restricted specialization,...
rspcva 3522 Restricted specialization,...
rspccva 3523 Restricted specialization,...
rspcev 3524 Restricted existential spe...
rspcevOLD 3525 Obsolete version of ~ rspc...
rspcdva 3526 Restricted specialization,...
rspcedvd 3527 Restricted existential spe...
rspcime 3528 Prove a restricted existen...
rspceaimv 3529 Restricted existential spe...
rspcedeq1vd 3530 Restricted existential spe...
rspcedeq2vd 3531 Restricted existential spe...
rspc2 3532 Restricted specialization ...
rspc2gv 3533 Restricted specialization ...
rspc2v 3534 2-variable restricted spec...
rspc2va 3535 2-variable restricted spec...
rspc2ev 3536 2-variable restricted exis...
rspc3v 3537 3-variable restricted spec...
rspc3ev 3538 3-variable restricted exis...
rspceeqv 3539 Restricted existential spe...
ralxpxfr2d 3540 Transfer a universal quant...
rexraleqim 3541 Statement following from e...
eqvincg 3542 A variable introduction la...
eqvinc 3543 A variable introduction la...
eqvincf 3544 A variable introduction la...
alexeqg 3545 Two ways to express substi...
ceqex 3546 Equality implies equivalen...
ceqsexg 3547 A representation of explic...
ceqsexgv 3548 Elimination of an existent...
ceqsexgvOLD 3549 Obsolete version of ~ ceqs...
ceqsrexv 3550 Elimination of a restricte...
ceqsrexbv 3551 Elimination of a restricte...
ceqsrex2v 3552 Elimination of a restricte...
clel2g 3553 Alternate definition of me...
clel2gOLD 3554 Obsolete version of ~ clel...
clel2 3555 Alternate definition of me...
clel3g 3556 Alternate definition of me...
clel3 3557 Alternate definition of me...
clel4g 3558 Alternate definition of me...
clel4 3559 Alternate definition of me...
clel4OLD 3560 Obsolete version of ~ clel...
clel5 3561 Alternate definition of cl...
pm13.183 3562 Compare theorem *13.183 in...
rr19.3v 3563 Restricted quantifier vers...
rr19.28v 3564 Restricted quantifier vers...
elabgt 3565 Membership in a class abst...
elabgf 3566 Membership in a class abst...
elabf 3567 Membership in a class abst...
elabgw 3568 Membership in a class abst...
elab2gw 3569 Membership in a class abst...
elabg 3570 Membership in a class abst...
elab 3571 Membership in a class abst...
elab2g 3572 Membership in a class abst...
elabd 3573 Explicit demonstration the...
elab2 3574 Membership in a class abst...
elab4g 3575 Membership in a class abst...
elab3gf 3576 Membership in a class abst...
elab3g 3577 Membership in a class abst...
elab3 3578 Membership in a class abst...
elrabi 3579 Implication for the member...
elrabiOLD 3580 Obsolete version of ~ elra...
elrabf 3581 Membership in a restricted...
rabtru 3582 Abstract builder using the...
rabeqc 3583 A restricted class abstrac...
elrab3t 3584 Membership in a restricted...
elrab 3585 Membership in a restricted...
elrab3 3586 Membership in a restricted...
elrabd 3587 Membership in a restricted...
elrab2 3588 Membership in a restricted...
elrab2w 3589 Membership in a restricted...
ralab 3590 Universal quantification o...
ralrab 3591 Universal quantification o...
rexab 3592 Existential quantification...
rexrab 3593 Existential quantification...
ralab2 3594 Universal quantification o...
ralab2OLD 3595 Obsolete version of ~ rala...
ralrab2 3596 Universal quantification o...
rexab2 3597 Existential quantification...
rexab2OLD 3598 Obsolete version of ~ rexa...
rexrab2 3599 Existential quantification...
abidnf 3600 Identity used to create cl...
dedhb 3601 A deduction theorem for co...
nelrdva 3602 Deduce negative membership...
eqeu 3603 A condition which implies ...
moeq 3604 There exists at most one s...
eueq 3605 A class is a set if and on...
eueqi 3606 There exists a unique set ...
eueq2 3607 Equality has existential u...
eueq3 3608 Equality has existential u...
moeq3 3609 "At most one" property of ...
mosub 3610 "At most one" remains true...
mo2icl 3611 Theorem for inferring "at ...
mob2 3612 Consequence of "at most on...
moi2 3613 Consequence of "at most on...
mob 3614 Equality implied by "at mo...
moi 3615 Equality implied by "at mo...
morex 3616 Derive membership from uni...
euxfr2w 3617 Transfer existential uniqu...
euxfrw 3618 Transfer existential uniqu...
euxfr2 3619 Transfer existential uniqu...
euxfr 3620 Transfer existential uniqu...
euind 3621 Existential uniqueness via...
reu2 3622 A way to express restricte...
reu6 3623 A way to express restricte...
reu3 3624 A way to express restricte...
reu6i 3625 A condition which implies ...
eqreu 3626 A condition which implies ...
rmo4 3627 Restricted "at most one" u...
reu4 3628 Restricted uniqueness usin...
reu7 3629 Restricted uniqueness usin...
reu8 3630 Restricted uniqueness usin...
rmo3f 3631 Restricted "at most one" u...
rmo4f 3632 Restricted "at most one" u...
reu2eqd 3633 Deduce equality from restr...
reueq 3634 Equality has existential u...
rmoeq 3635 Equality's restricted exis...
rmoan 3636 Restricted "at most one" s...
rmoim 3637 Restricted "at most one" i...
rmoimia 3638 Restricted "at most one" i...
rmoimi 3639 Restricted "at most one" i...
rmoimi2 3640 Restricted "at most one" i...
2reu5a 3641 Double restricted existent...
reuimrmo 3642 Restricted uniqueness impl...
2reuswap 3643 A condition allowing swap ...
2reuswap2 3644 A condition allowing swap ...
reuxfrd 3645 Transfer existential uniqu...
reuxfr 3646 Transfer existential uniqu...
reuxfr1d 3647 Transfer existential uniqu...
reuxfr1ds 3648 Transfer existential uniqu...
reuxfr1 3649 Transfer existential uniqu...
reuind 3650 Existential uniqueness via...
2rmorex 3651 Double restricted quantifi...
2reu5lem1 3652 Lemma for ~ 2reu5 . Note ...
2reu5lem2 3653 Lemma for ~ 2reu5 . (Cont...
2reu5lem3 3654 Lemma for ~ 2reu5 . This ...
2reu5 3655 Double restricted existent...
2reurex 3656 Double restricted quantifi...
2reurmo 3657 Double restricted quantifi...
2rmoswap 3658 A condition allowing to sw...
2rexreu 3659 Double restricted existent...
cdeqi 3662 Deduce conditional equalit...
cdeqri 3663 Property of conditional eq...
cdeqth 3664 Deduce conditional equalit...
cdeqnot 3665 Distribute conditional equ...
cdeqal 3666 Distribute conditional equ...
cdeqab 3667 Distribute conditional equ...
cdeqal1 3668 Distribute conditional equ...
cdeqab1 3669 Distribute conditional equ...
cdeqim 3670 Distribute conditional equ...
cdeqcv 3671 Conditional equality for s...
cdeqeq 3672 Distribute conditional equ...
cdeqel 3673 Distribute conditional equ...
nfcdeq 3674 If we have a conditional e...
nfccdeq 3675 Variation of ~ nfcdeq for ...
rru 3676 Relative version of Russel...
rruOLD 3677 Obsolete version of ~ rru ...
ru 3678 Russell's Paradox. Propos...
dfsbcq 3681 Proper substitution of a c...
dfsbcq2 3682 This theorem, which is sim...
sbsbc 3683 Show that ~ df-sb and ~ df...
sbceq1d 3684 Equality theorem for class...
sbceq1dd 3685 Equality theorem for class...
sbceqbid 3686 Equality theorem for class...
sbc8g 3687 This is the closest we can...
sbc2or 3688 The disjunction of two equ...
sbcex 3689 By our definition of prope...
sbceq1a 3690 Equality theorem for class...
sbceq2a 3691 Equality theorem for class...
spsbc 3692 Specialization: if a formu...
spsbcd 3693 Specialization: if a formu...
sbcth 3694 A substitution into a theo...
sbcthdv 3695 Deduction version of ~ sbc...
sbcid 3696 An identity theorem for su...
nfsbc1d 3697 Deduction version of ~ nfs...
nfsbc1 3698 Bound-variable hypothesis ...
nfsbc1v 3699 Bound-variable hypothesis ...
nfsbcdw 3700 Deduction version of ~ nfs...
nfsbcw 3701 Bound-variable hypothesis ...
sbccow 3702 A composition law for clas...
nfsbcd 3703 Deduction version of ~ nfs...
nfsbc 3704 Bound-variable hypothesis ...
sbcco 3705 A composition law for clas...
sbcco2 3706 A composition law for clas...
sbc5 3707 An equivalence for class s...
sbc5ALT 3708 Alternate proof of ~ sbc5 ...
sbc6g 3709 An equivalence for class s...
sbc6 3710 An equivalence for class s...
sbc7 3711 An equivalence for class s...
cbvsbcw 3712 Change bound variables in ...
cbvsbcvw 3713 Change the bound variable ...
cbvsbc 3714 Change bound variables in ...
cbvsbcv 3715 Change the bound variable ...
sbciegft 3716 Conversion of implicit sub...
sbciegf 3717 Conversion of implicit sub...
sbcieg 3718 Conversion of implicit sub...
sbcie2g 3719 Conversion of implicit sub...
sbcie 3720 Conversion of implicit sub...
sbciedf 3721 Conversion of implicit sub...
sbcied 3722 Conversion of implicit sub...
sbcied2 3723 Conversion of implicit sub...
elrabsf 3724 Membership in a restricted...
eqsbc3 3725 Substitution applied to an...
sbcng 3726 Move negation in and out o...
sbcimg 3727 Distribution of class subs...
sbcan 3728 Distribution of class subs...
sbcor 3729 Distribution of class subs...
sbcbig 3730 Distribution of class subs...
sbcn1 3731 Move negation in and out o...
sbcim1 3732 Distribution of class subs...
sbcbid 3733 Formula-building deduction...
sbcbidv 3734 Formula-building deduction...
sbcbidvOLD 3735 Obsolete version of ~ sbcb...
sbcbii 3736 Formula-building inference...
sbcbi1 3737 Distribution of class subs...
sbcbi2 3738 Substituting into equivale...
sbcbi2OLD 3739 Obsolete proof of ~ sbcbi2...
sbcal 3740 Move universal quantifier ...
sbcex2 3741 Move existential quantifie...
sbceqal 3742 Class version of one impli...
sbeqalb 3743 Theorem *14.121 in [Whiteh...
eqsbc3r 3744 ~ eqsbc3 with setvar varia...
sbc3an 3745 Distribution of class subs...
sbcel1v 3746 Class substitution into a ...
sbcel2gv 3747 Class substitution into a ...
sbcel21v 3748 Class substitution into a ...
sbcimdv 3749 Substitution analogue of T...
sbctt 3750 Substitution for a variabl...
sbcgf 3751 Substitution for a variabl...
sbc19.21g 3752 Substitution for a variabl...
sbcg 3753 Substitution for a variabl...
sbcgfi 3754 Substitution for a variabl...
sbc2iegf 3755 Conversion of implicit sub...
sbc2ie 3756 Conversion of implicit sub...
sbc2iedv 3757 Conversion of implicit sub...
sbc3ie 3758 Conversion of implicit sub...
sbccomlem 3759 Lemma for ~ sbccom . (Con...
sbccom 3760 Commutative law for double...
sbcralt 3761 Interchange class substitu...
sbcrext 3762 Interchange class substitu...
sbcralg 3763 Interchange class substitu...
sbcrex 3764 Interchange class substitu...
sbcreu 3765 Interchange class substitu...
reu8nf 3766 Restricted uniqueness usin...
sbcabel 3767 Interchange class substitu...
rspsbc 3768 Restricted quantifier vers...
rspsbca 3769 Restricted quantifier vers...
rspesbca 3770 Existence form of ~ rspsbc...
spesbc 3771 Existence form of ~ spsbc ...
spesbcd 3772 form of ~ spsbc . (Contri...
sbcth2 3773 A substitution into a theo...
ra4v 3774 Version of ~ ra4 with a di...
ra4 3775 Restricted quantifier vers...
rmo2 3776 Alternate definition of re...
rmo2i 3777 Condition implying restric...
rmo3 3778 Restricted "at most one" u...
rmob 3779 Consequence of "at most on...
rmoi 3780 Consequence of "at most on...
rmob2 3781 Consequence of "restricted...
rmoi2 3782 Consequence of "restricted...
rmoanim 3783 Introduction of a conjunct...
rmoanimALT 3784 Alternate proof of ~ rmoan...
reuan 3785 Introduction of a conjunct...
2reu1 3786 Double restricted existent...
2reu2 3787 Double restricted existent...
csb2 3790 Alternate expression for t...
csbeq1 3791 Analogue of ~ dfsbcq for p...
csbeq1d 3792 Equality deduction for pro...
csbeq2 3793 Substituting into equivale...
csbeq2d 3794 Formula-building deduction...
csbeq2dv 3795 Formula-building deduction...
csbeq2i 3796 Formula-building inference...
csbeq12dv 3797 Formula-building inference...
cbvcsbw 3798 Change bound variables in ...
cbvcsb 3799 Change bound variables in ...
cbvcsbv 3800 Change the bound variable ...
csbid 3801 Analogue of ~ sbid for pro...
csbeq1a 3802 Equality theorem for prope...
csbcow 3803 Composition law for chaine...
csbco 3804 Composition law for chaine...
csbtt 3805 Substitution doesn't affec...
csbconstgf 3806 Substitution doesn't affec...
csbconstg 3807 Substitution doesn't affec...
csbgfi 3808 Substitution for a variabl...
csbconstgi 3809 The proper substitution of...
nfcsb1d 3810 Bound-variable hypothesis ...
nfcsb1 3811 Bound-variable hypothesis ...
nfcsb1v 3812 Bound-variable hypothesis ...
nfcsbd 3813 Deduction version of ~ nfc...
nfcsbw 3814 Bound-variable hypothesis ...
nfcsb 3815 Bound-variable hypothesis ...
csbhypf 3816 Introduce an explicit subs...
csbiebt 3817 Conversion of implicit sub...
csbiedf 3818 Conversion of implicit sub...
csbieb 3819 Bidirectional conversion b...
csbiebg 3820 Bidirectional conversion b...
csbiegf 3821 Conversion of implicit sub...
csbief 3822 Conversion of implicit sub...
csbie 3823 Conversion of implicit sub...
csbied 3824 Conversion of implicit sub...
csbied2 3825 Conversion of implicit sub...
csbie2t 3826 Conversion of implicit sub...
csbie2 3827 Conversion of implicit sub...
csbie2g 3828 Conversion of implicit sub...
cbvrabcsfw 3829 Version of ~ cbvrabcsf wit...
cbvralcsf 3830 A more general version of ...
cbvrexcsf 3831 A more general version of ...
cbvreucsf 3832 A more general version of ...
cbvrabcsf 3833 A more general version of ...
cbvralv2 3834 Rule used to change the bo...
cbvrexv2 3835 Rule used to change the bo...
vtocl2dOLD 3836 Obsolete version of ~ vtoc...
rspc2vd 3837 Deduction version of 2-var...
difjust 3843 Soundness justification th...
unjust 3845 Soundness justification th...
injust 3847 Soundness justification th...
dfin5 3849 Alternate definition for t...
dfdif2 3850 Alternate definition of cl...
eldif 3851 Expansion of membership in...
eldifd 3852 If a class is in one class...
eldifad 3853 If a class is in the diffe...
eldifbd 3854 If a class is in the diffe...
elneeldif 3855 The elements of a set diff...
velcomp 3856 Characterization of setvar...
elin 3857 Expansion of membership in...
dfss 3859 Variant of subclass defini...
dfss2 3861 Alternate definition of th...
dfss2OLD 3862 Obsolete version of ~ dfss...
dfss3 3863 Alternate definition of su...
dfss6 3864 Alternate definition of su...
dfss2f 3865 Equivalence for subclass r...
dfss3f 3866 Equivalence for subclass r...
nfss 3867 If ` x ` is not free in ` ...
ssel 3868 Membership relationships f...
sselOLD 3869 Obsolete version of ~ ssel...
ssel2 3870 Membership relationships f...
sseli 3871 Membership implication fro...
sselii 3872 Membership inference from ...
sseldi 3873 Membership inference from ...
sseld 3874 Membership deduction from ...
sselda 3875 Membership deduction from ...
sseldd 3876 Membership inference from ...
ssneld 3877 If a class is not in anoth...
ssneldd 3878 If an element is not in a ...
ssriv 3879 Inference based on subclas...
ssrd 3880 Deduction based on subclas...
ssrdv 3881 Deduction based on subclas...
sstr2 3882 Transitivity of subclass r...
sstr 3883 Transitivity of subclass r...
sstri 3884 Subclass transitivity infe...
sstrd 3885 Subclass transitivity dedu...
sstrid 3886 Subclass transitivity dedu...
sstrdi 3887 Subclass transitivity dedu...
sylan9ss 3888 A subclass transitivity de...
sylan9ssr 3889 A subclass transitivity de...
eqss 3890 The subclass relationship ...
eqssi 3891 Infer equality from two su...
eqssd 3892 Equality deduction from tw...
sssseq 3893 If a class is a subclass o...
eqrd 3894 Deduce equality of classes...
eqri 3895 Infer equality of classes ...
eqelssd 3896 Equality deduction from su...
ssid 3897 Any class is a subclass of...
ssidd 3898 Weakening of ~ ssid . (Co...
ssv 3899 Any class is a subclass of...
sseq1 3900 Equality theorem for subcl...
sseq2 3901 Equality theorem for the s...
sseq12 3902 Equality theorem for the s...
sseq1i 3903 An equality inference for ...
sseq2i 3904 An equality inference for ...
sseq12i 3905 An equality inference for ...
sseq1d 3906 An equality deduction for ...
sseq2d 3907 An equality deduction for ...
sseq12d 3908 An equality deduction for ...
eqsstri 3909 Substitution of equality i...
eqsstrri 3910 Substitution of equality i...
sseqtri 3911 Substitution of equality i...
sseqtrri 3912 Substitution of equality i...
eqsstrd 3913 Substitution of equality i...
eqsstrrd 3914 Substitution of equality i...
sseqtrd 3915 Substitution of equality i...
sseqtrrd 3916 Substitution of equality i...
3sstr3i 3917 Substitution of equality i...
3sstr4i 3918 Substitution of equality i...
3sstr3g 3919 Substitution of equality i...
3sstr4g 3920 Substitution of equality i...
3sstr3d 3921 Substitution of equality i...
3sstr4d 3922 Substitution of equality i...
eqsstrid 3923 A chained subclass and equ...
eqsstrrid 3924 A chained subclass and equ...
sseqtrdi 3925 A chained subclass and equ...
sseqtrrdi 3926 A chained subclass and equ...
sseqtrid 3927 Subclass transitivity dedu...
sseqtrrid 3928 Subclass transitivity dedu...
eqsstrdi 3929 A chained subclass and equ...
eqsstrrdi 3930 A chained subclass and equ...
eqimss 3931 Equality implies the subcl...
eqimss2 3932 Equality implies the subcl...
eqimssi 3933 Infer subclass relationshi...
eqimss2i 3934 Infer subclass relationshi...
nssne1 3935 Two classes are different ...
nssne2 3936 Two classes are different ...
nss 3937 Negation of subclass relat...
nelss 3938 Demonstrate by witnesses t...
ssrexf 3939 Restricted existential qua...
ssrmof 3940 "At most one" existential ...
ssralv 3941 Quantification restricted ...
ssrexv 3942 Existential quantification...
ss2ralv 3943 Two quantifications restri...
ss2rexv 3944 Two existential quantifica...
ralss 3945 Restricted universal quant...
rexss 3946 Restricted existential qua...
ss2ab 3947 Class abstractions in a su...
abss 3948 Class abstraction in a sub...
ssab 3949 Subclass of a class abstra...
ssabral 3950 The relation for a subclas...
ss2abdv 3951 Deduction of abstraction s...
ss2abdvALT 3952 Alternate proof of ~ ss2ab...
ss2abdvOLD 3953 Obsolete version of ~ ss2a...
ss2abi 3954 Inference of abstraction s...
ss2abiOLD 3955 Obsolete version of ~ ss2a...
abssdv 3956 Deduction of abstraction s...
abssi 3957 Inference of abstraction s...
ss2rab 3958 Restricted abstraction cla...
rabss 3959 Restricted class abstracti...
ssrab 3960 Subclass of a restricted c...
ssrabdv 3961 Subclass of a restricted c...
rabssdv 3962 Subclass of a restricted c...
ss2rabdv 3963 Deduction of restricted ab...
ss2rabi 3964 Inference of restricted ab...
rabss2 3965 Subclass law for restricte...
ssab2 3966 Subclass relation for the ...
ssrab2 3967 Subclass relation for a re...
ssrab2OLD 3968 Obsolete version of ~ ssra...
ssrab3 3969 Subclass relation for a re...
rabssrabd 3970 Subclass of a restricted c...
ssrabeq 3971 If the restricting class o...
rabssab 3972 A restricted class is a su...
uniiunlem 3973 A subset relationship usef...
dfpss2 3974 Alternate definition of pr...
dfpss3 3975 Alternate definition of pr...
psseq1 3976 Equality theorem for prope...
psseq2 3977 Equality theorem for prope...
psseq1i 3978 An equality inference for ...
psseq2i 3979 An equality inference for ...
psseq12i 3980 An equality inference for ...
psseq1d 3981 An equality deduction for ...
psseq2d 3982 An equality deduction for ...
psseq12d 3983 An equality deduction for ...
pssss 3984 A proper subclass is a sub...
pssne 3985 Two classes in a proper su...
pssssd 3986 Deduce subclass from prope...
pssned 3987 Proper subclasses are uneq...
sspss 3988 Subclass in terms of prope...
pssirr 3989 Proper subclass is irrefle...
pssn2lp 3990 Proper subclass has no 2-c...
sspsstri 3991 Two ways of stating tricho...
ssnpss 3992 Partial trichotomy law for...
psstr 3993 Transitive law for proper ...
sspsstr 3994 Transitive law for subclas...
psssstr 3995 Transitive law for subclas...
psstrd 3996 Proper subclass inclusion ...
sspsstrd 3997 Transitivity involving sub...
psssstrd 3998 Transitivity involving sub...
npss 3999 A class is not a proper su...
ssnelpss 4000 A subclass missing a membe...
ssnelpssd 4001 Subclass inclusion with on...
ssexnelpss 4002 If there is an element of ...
dfdif3 4003 Alternate definition of cl...
difeq1 4004 Equality theorem for class...
difeq2 4005 Equality theorem for class...
difeq12 4006 Equality theorem for class...
difeq1i 4007 Inference adding differenc...
difeq2i 4008 Inference adding differenc...
difeq12i 4009 Equality inference for cla...
difeq1d 4010 Deduction adding differenc...
difeq2d 4011 Deduction adding differenc...
difeq12d 4012 Equality deduction for cla...
difeqri 4013 Inference from membership ...
nfdif 4014 Bound-variable hypothesis ...
eldifi 4015 Implication of membership ...
eldifn 4016 Implication of membership ...
elndif 4017 A set does not belong to a...
neldif 4018 Implication of membership ...
difdif 4019 Double class difference. ...
difss 4020 Subclass relationship for ...
difssd 4021 A difference of two classe...
difss2 4022 If a class is contained in...
difss2d 4023 If a class is contained in...
ssdifss 4024 Preservation of a subclass...
ddif 4025 Double complement under un...
ssconb 4026 Contraposition law for sub...
sscon 4027 Contraposition law for sub...
ssdif 4028 Difference law for subsets...
ssdifd 4029 If ` A ` is contained in `...
sscond 4030 If ` A ` is contained in `...
ssdifssd 4031 If ` A ` is contained in `...
ssdif2d 4032 If ` A ` is contained in `...
raldifb 4033 Restricted universal quant...
rexdifi 4034 Restricted existential qua...
complss 4035 Complementation reverses i...
compleq 4036 Two classes are equal if a...
elun 4037 Expansion of membership in...
elunnel1 4038 A member of a union that i...
uneqri 4039 Inference from membership ...
unidm 4040 Idempotent law for union o...
uncom 4041 Commutative law for union ...
equncom 4042 If a class equals the unio...
equncomi 4043 Inference form of ~ equnco...
uneq1 4044 Equality theorem for the u...
uneq2 4045 Equality theorem for the u...
uneq12 4046 Equality theorem for the u...
uneq1i 4047 Inference adding union to ...
uneq2i 4048 Inference adding union to ...
uneq12i 4049 Equality inference for the...
uneq1d 4050 Deduction adding union to ...
uneq2d 4051 Deduction adding union to ...
uneq12d 4052 Equality deduction for the...
nfun 4053 Bound-variable hypothesis ...
unass 4054 Associative law for union ...
un12 4055 A rearrangement of union. ...
un23 4056 A rearrangement of union. ...
un4 4057 A rearrangement of the uni...
unundi 4058 Union distributes over its...
unundir 4059 Union distributes over its...
ssun1 4060 Subclass relationship for ...
ssun2 4061 Subclass relationship for ...
ssun3 4062 Subclass law for union of ...
ssun4 4063 Subclass law for union of ...
elun1 4064 Membership law for union o...
elun2 4065 Membership law for union o...
elunant 4066 A statement is true for ev...
unss1 4067 Subclass law for union of ...
ssequn1 4068 A relationship between sub...
unss2 4069 Subclass law for union of ...
unss12 4070 Subclass law for union of ...
ssequn2 4071 A relationship between sub...
unss 4072 The union of two subclasse...
unssi 4073 An inference showing the u...
unssd 4074 A deduction showing the un...
unssad 4075 If ` ( A u. B ) ` is conta...
unssbd 4076 If ` ( A u. B ) ` is conta...
ssun 4077 A condition that implies i...
rexun 4078 Restricted existential qua...
ralunb 4079 Restricted quantification ...
ralun 4080 Restricted quantification ...
elini 4081 Membership in an intersect...
elind 4082 Deduce membership in an in...
elinel1 4083 Membership in an intersect...
elinel2 4084 Membership in an intersect...
elin2 4085 Membership in a class defi...
elin1d 4086 Elementhood in the first s...
elin2d 4087 Elementhood in the first s...
elin3 4088 Membership in a class defi...
incom 4089 Commutative law for inters...
incomOLD 4090 Obsolete version of ~ inco...
ineqcom 4091 Two ways of expressing tha...
ineqcomi 4092 Two ways of expressing tha...
ineqri 4093 Inference from membership ...
ineq1 4094 Equality theorem for inter...
ineq2 4095 Equality theorem for inter...
ineq12 4096 Equality theorem for inter...
ineq1i 4097 Equality inference for int...
ineq2i 4098 Equality inference for int...
ineq12i 4099 Equality inference for int...
ineq1d 4100 Equality deduction for int...
ineq2d 4101 Equality deduction for int...
ineq12d 4102 Equality deduction for int...
ineqan12d 4103 Equality deduction for int...
sseqin2 4104 A relationship between sub...
nfin 4105 Bound-variable hypothesis ...
rabbi2dva 4106 Deduction from a wff to a ...
inidm 4107 Idempotent law for interse...
inass 4108 Associative law for inters...
in12 4109 A rearrangement of interse...
in32 4110 A rearrangement of interse...
in13 4111 A rearrangement of interse...
in31 4112 A rearrangement of interse...
inrot 4113 Rotate the intersection of...
in4 4114 Rearrangement of intersect...
inindi 4115 Intersection distributes o...
inindir 4116 Intersection distributes o...
inss1 4117 The intersection of two cl...
inss2 4118 The intersection of two cl...
ssin 4119 Subclass of intersection. ...
ssini 4120 An inference showing that ...
ssind 4121 A deduction showing that a...
ssrin 4122 Add right intersection to ...
sslin 4123 Add left intersection to s...
ssrind 4124 Add right intersection to ...
ss2in 4125 Intersection of subclasses...
ssinss1 4126 Intersection preserves sub...
inss 4127 Inclusion of an intersecti...
rexin 4128 Restricted existential qua...
dfss7 4129 Alternate definition of su...
symdifcom 4132 Symmetric difference commu...
symdifeq1 4133 Equality theorem for symme...
symdifeq2 4134 Equality theorem for symme...
nfsymdif 4135 Hypothesis builder for sym...
elsymdif 4136 Membership in a symmetric ...
dfsymdif4 4137 Alternate definition of th...
elsymdifxor 4138 Membership in a symmetric ...
dfsymdif2 4139 Alternate definition of th...
symdifass 4140 Symmetric difference is as...
difsssymdif 4141 The symmetric difference c...
difsymssdifssd 4142 If the symmetric differenc...
unabs 4143 Absorption law for union. ...
inabs 4144 Absorption law for interse...
nssinpss 4145 Negation of subclass expre...
nsspssun 4146 Negation of subclass expre...
dfss4 4147 Subclass defined in terms ...
dfun2 4148 An alternate definition of...
dfin2 4149 An alternate definition of...
difin 4150 Difference with intersecti...
ssdifim 4151 Implication of a class dif...
ssdifsym 4152 Symmetric class difference...
dfss5 4153 Alternate definition of su...
dfun3 4154 Union defined in terms of ...
dfin3 4155 Intersection defined in te...
dfin4 4156 Alternate definition of th...
invdif 4157 Intersection with universa...
indif 4158 Intersection with class di...
indif2 4159 Bring an intersection in a...
indif1 4160 Bring an intersection in a...
indifcom 4161 Commutation law for inters...
indi 4162 Distributive law for inter...
undi 4163 Distributive law for union...
indir 4164 Distributive law for inter...
undir 4165 Distributive law for union...
unineq 4166 Infer equality from equali...
uneqin 4167 Equality of union and inte...
difundi 4168 Distributive law for class...
difundir 4169 Distributive law for class...
difindi 4170 Distributive law for class...
difindir 4171 Distributive law for class...
indifdi 4172 Distribute intersection ov...
indifdir 4173 Distribute intersection ov...
indifdirOLD 4174 Obsolete version of ~ indi...
difdif2 4175 Class difference by a clas...
undm 4176 De Morgan's law for union....
indm 4177 De Morgan's law for inters...
difun1 4178 A relationship involving d...
undif3 4179 An equality involving clas...
difin2 4180 Represent a class differen...
dif32 4181 Swap second and third argu...
difabs 4182 Absorption-like law for cl...
sscon34b 4183 Relative complementation r...
rcompleq 4184 Two subclasses are equal i...
dfsymdif3 4185 Alternate definition of th...
unab 4186 Union of two class abstrac...
inab 4187 Intersection of two class ...
difab 4188 Difference of two class ab...
abanssl 4189 A class abstraction with a...
abanssr 4190 A class abstraction with a...
notab 4191 A class abstraction define...
unrab 4192 Union of two restricted cl...
inrab 4193 Intersection of two restri...
inrab2 4194 Intersection with a restri...
difrab 4195 Difference of two restrict...
dfrab3 4196 Alternate definition of re...
dfrab2 4197 Alternate definition of re...
notrab 4198 Complementation of restric...
dfrab3ss 4199 Restricted class abstracti...
rabun2 4200 Abstraction restricted to ...
reuss2 4201 Transfer uniqueness to a s...
reuss 4202 Transfer uniqueness to a s...
reuun1 4203 Transfer uniqueness to a s...
reuun2 4204 Transfer uniqueness to a s...
reupick 4205 Restricted uniqueness "pic...
reupick3 4206 Restricted uniqueness "pic...
reupick2 4207 Restricted uniqueness "pic...
euelss 4208 Transfer uniqueness of an ...
dfnul4 4211 Alternate definition of th...
dfnul2 4212 Alternate definition of th...
dfnul3 4213 Alternate definition of th...
dfnul2OLD 4214 Obsolete version of ~ dfnu...
dfnul3OLD 4215 Obsolete version of ~ dfnu...
dfnul4OLD 4216 Obsolete version of ~ dfnu...
noel 4217 The empty set has no eleme...
noelOLD 4218 Obsolete version of ~ noel...
nel02 4219 The empty set has no eleme...
n0i 4220 If a class has elements, t...
ne0i 4221 If a class has elements, t...
ne0d 4222 Deduction form of ~ ne0i ....
n0ii 4223 If a class has elements, t...
ne0ii 4224 If a class has elements, t...
vn0 4225 The universal class is not...
vn0ALT 4226 Alternate proof of ~ vn0 ....
eq0f 4227 A class is equal to the em...
neq0f 4228 A class is not empty if an...
n0f 4229 A class is nonempty if and...
eq0 4230 A class is equal to the em...
eq0ALT 4231 Alternate proof of ~ eq0 ....
neq0 4232 A class is not empty if an...
n0 4233 A class is nonempty if and...
eq0OLDOLD 4234 Obsolete version of ~ eq0 ...
neq0OLD 4235 Obsolete version of ~ neq0...
n0OLD 4236 Obsolete version of ~ n0 a...
nel0 4237 From the general negation ...
reximdva0 4238 Restricted existence deduc...
rspn0 4239 Specialization for restric...
rspn0OLD 4240 Obsolete version of ~ rspn...
n0rex 4241 There is an element in a n...
ssn0rex 4242 There is an element in a c...
n0moeu 4243 A case of equivalence of "...
rex0 4244 Vacuous restricted existen...
reu0 4245 Vacuous restricted uniquen...
rmo0 4246 Vacuous restricted at-most...
0el 4247 Membership of the empty se...
n0el 4248 Negated membership of the ...
eqeuel 4249 A condition which implies ...
ssdif0 4250 Subclass expressed in term...
difn0 4251 If the difference of two s...
pssdifn0 4252 A proper subclass has a no...
pssdif 4253 A proper subclass has a no...
ndisj 4254 Express that an intersecti...
difin0ss 4255 Difference, intersection, ...
inssdif0 4256 Intersection, subclass, an...
difid 4257 The difference between a c...
difidALT 4258 Alternate proof of ~ difid...
dif0 4259 The difference between a c...
ab0 4260 The class of sets verifyin...
ab0OLD 4261 Obsolete version of ~ ab0 ...
ab0ALT 4262 Alternate proof of ~ ab0 ,...
dfnf5 4263 Characterization of nonfre...
ab0orv 4264 The class abstraction defi...
ab0orvALT 4265 Alternate proof of ~ ab0or...
abn0 4266 Nonempty class abstraction...
abn0OLD 4267 Obsolete version of ~ abn0...
rab0 4268 Any restricted class abstr...
rabeq0w 4269 Condition for a restricted...
rabeq0 4270 Condition for a restricted...
rabn0 4271 Nonempty restricted class ...
rabxm 4272 Law of excluded middle, in...
rabnc 4273 Law of noncontradiction, i...
elneldisj 4274 The set of elements ` s ` ...
elnelun 4275 The union of the set of el...
un0 4276 The union of a class with ...
in0 4277 The intersection of a clas...
0un 4278 The union of the empty set...
0in 4279 The intersection of the em...
inv1 4280 The intersection of a clas...
unv 4281 The union of a class with ...
0ss 4282 The null set is a subset o...
ss0b 4283 Any subset of the empty se...
ss0 4284 Any subset of the empty se...
sseq0 4285 A subclass of an empty cla...
ssn0 4286 A class with a nonempty su...
0dif 4287 The difference between the...
abf 4288 A class abstraction determ...
abfOLD 4289 Obsolete version of ~ abf ...
eq0rdv 4290 Deduction for equality to ...
eq0rdvALT 4291 Alternate proof of ~ eq0rd...
csbprc 4292 The proper substitution of...
csb0 4293 The proper substitution of...
csb0OLD 4294 Obsolete version of ~ csb0...
sbcel12 4295 Distribute proper substitu...
sbceqg 4296 Distribute proper substitu...
sbceqi 4297 Distribution of class subs...
sbcnel12g 4298 Distribute proper substitu...
sbcne12 4299 Distribute proper substitu...
sbcel1g 4300 Move proper substitution i...
sbceq1g 4301 Move proper substitution t...
sbcel2 4302 Move proper substitution i...
sbceq2g 4303 Move proper substitution t...
csbcom 4304 Commutative law for double...
sbcnestgfw 4305 Nest the composition of tw...
csbnestgfw 4306 Nest the composition of tw...
sbcnestgw 4307 Nest the composition of tw...
csbnestgw 4308 Nest the composition of tw...
sbcco3gw 4309 Composition of two substit...
sbcnestgf 4310 Nest the composition of tw...
csbnestgf 4311 Nest the composition of tw...
sbcnestg 4312 Nest the composition of tw...
csbnestg 4313 Nest the composition of tw...
sbcco3g 4314 Composition of two substit...
csbco3g 4315 Composition of two class s...
csbnest1g 4316 Nest the composition of tw...
csbidm 4317 Idempotent law for class s...
csbvarg 4318 The proper substitution of...
csbvargi 4319 The proper substitution of...
sbccsb 4320 Substitution into a wff ex...
sbccsb2 4321 Substitution into a wff ex...
rspcsbela 4322 Special case related to ~ ...
sbnfc2 4323 Two ways of expressing " `...
csbab 4324 Move substitution into a c...
csbun 4325 Distribution of class subs...
csbin 4326 Distribute proper substitu...
csbie2df 4327 Conversion of implicit sub...
2nreu 4328 If there are two different...
un00 4329 Two classes are empty iff ...
vss 4330 Only the universal class h...
0pss 4331 The null set is a proper s...
npss0 4332 No set is a proper subset ...
pssv 4333 Any non-universal class is...
disj 4334 Two ways of saying that tw...
disjOLD 4335 Obsolete version of ~ disj...
disjr 4336 Two ways of saying that tw...
disj1 4337 Two ways of saying that tw...
reldisj 4338 Two ways of saying that tw...
reldisjOLD 4339 Obsolete version of ~ reld...
disj3 4340 Two ways of saying that tw...
disjne 4341 Members of disjoint sets a...
disjeq0 4342 Two disjoint sets are equa...
disjel 4343 A set can't belong to both...
disj2 4344 Two ways of saying that tw...
disj4 4345 Two ways of saying that tw...
ssdisj 4346 Intersection with a subcla...
disjpss 4347 A class is a proper subset...
undisj1 4348 The union of disjoint clas...
undisj2 4349 The union of disjoint clas...
ssindif0 4350 Subclass expressed in term...
inelcm 4351 The intersection of classe...
minel 4352 A minimum element of a cla...
undif4 4353 Distribute union over diff...
disjssun 4354 Subset relation for disjoi...
vdif0 4355 Universal class equality i...
difrab0eq 4356 If the difference between ...
pssnel 4357 A proper subclass has a me...
disjdif 4358 A class and its relative c...
disjdifr 4359 A class and its relative c...
difin0 4360 The difference of a class ...
unvdif 4361 The union of a class and i...
undif1 4362 Absorption of difference b...
undif2 4363 Absorption of difference b...
undifabs 4364 Absorption of difference b...
inundif 4365 The intersection and class...
disjdif2 4366 The difference of a class ...
difun2 4367 Absorption of union by dif...
undif 4368 Union of complementary par...
ssdifin0 4369 A subset of a difference d...
ssdifeq0 4370 A class is a subclass of i...
ssundif 4371 A condition equivalent to ...
difcom 4372 Swap the arguments of a cl...
pssdifcom1 4373 Two ways to express overla...
pssdifcom2 4374 Two ways to express non-co...
difdifdir 4375 Distributive law for class...
uneqdifeq 4376 Two ways to say that ` A `...
raldifeq 4377 Equality theorem for restr...
r19.2z 4378 Theorem 19.2 of [Margaris]...
r19.2zb 4379 A response to the notion t...
r19.3rz 4380 Restricted quantification ...
r19.28z 4381 Restricted quantifier vers...
r19.3rzv 4382 Restricted quantification ...
r19.9rzv 4383 Restricted quantification ...
r19.28zv 4384 Restricted quantifier vers...
r19.37zv 4385 Restricted quantifier vers...
r19.45zv 4386 Restricted version of Theo...
r19.44zv 4387 Restricted version of Theo...
r19.27z 4388 Restricted quantifier vers...
r19.27zv 4389 Restricted quantifier vers...
r19.36zv 4390 Restricted quantifier vers...
ralidmw 4391 Idempotent law for restric...
rzal 4392 Vacuous quantification is ...
rzalALT 4393 Alternate proof of ~ rzal ...
rexn0 4394 Restricted existential qua...
ralidm 4395 Idempotent law for restric...
ral0 4396 Vacuous universal quantifi...
ralf0 4397 The quantification of a fa...
rexn0OLD 4398 Obsolete version of ~ rexn...
ralidmOLD 4399 Obsolete version of ~ rali...
ral0OLD 4400 Obsolete version of ~ ral0...
ralf0OLD 4401 Obsolete version of ~ ralf...
ralnralall 4402 A contradiction concerning...
falseral0 4403 A false statement can only...
raaan 4404 Rearrange restricted quant...
raaanv 4405 Rearrange restricted quant...
sbss 4406 Set substitution into the ...
sbcssg 4407 Distribute proper substitu...
raaan2 4408 Rearrange restricted quant...
2reu4lem 4409 Lemma for ~ 2reu4 . (Cont...
2reu4 4410 Definition of double restr...
dfif2 4413 An alternate definition of...
dfif6 4414 An alternate definition of...
ifeq1 4415 Equality theorem for condi...
ifeq2 4416 Equality theorem for condi...
iftrue 4417 Value of the conditional o...
iftruei 4418 Inference associated with ...
iftrued 4419 Value of the conditional o...
iffalse 4420 Value of the conditional o...
iffalsei 4421 Inference associated with ...
iffalsed 4422 Value of the conditional o...
ifnefalse 4423 When values are unequal, b...
ifsb 4424 Distribute a function over...
dfif3 4425 Alternate definition of th...
dfif4 4426 Alternate definition of th...
dfif5 4427 Alternate definition of th...
ifssun 4428 A conditional class is inc...
ifeq12 4429 Equality theorem for condi...
ifeq1d 4430 Equality deduction for con...
ifeq2d 4431 Equality deduction for con...
ifeq12d 4432 Equality deduction for con...
ifbi 4433 Equivalence theorem for co...
ifbid 4434 Equivalence deduction for ...
ifbieq1d 4435 Equivalence/equality deduc...
ifbieq2i 4436 Equivalence/equality infer...
ifbieq2d 4437 Equivalence/equality deduc...
ifbieq12i 4438 Equivalence deduction for ...
ifbieq12d 4439 Equivalence deduction for ...
nfifd 4440 Deduction form of ~ nfif ....
nfif 4441 Bound-variable hypothesis ...
ifeq1da 4442 Conditional equality. (Co...
ifeq2da 4443 Conditional equality. (Co...
ifeq12da 4444 Equivalence deduction for ...
ifbieq12d2 4445 Equivalence deduction for ...
ifclda 4446 Conditional closure. (Con...
ifeqda 4447 Separation of the values o...
elimif 4448 Elimination of a condition...
ifbothda 4449 A wff ` th ` containing a ...
ifboth 4450 A wff ` th ` containing a ...
ifid 4451 Identical true and false a...
eqif 4452 Expansion of an equality w...
ifval 4453 Another expression of the ...
elif 4454 Membership in a conditiona...
ifel 4455 Membership of a conditiona...
ifcl 4456 Membership (closure) of a ...
ifcld 4457 Membership (closure) of a ...
ifcli 4458 Inference associated with ...
ifexd 4459 Existence of the condition...
ifexg 4460 Existence of the condition...
ifex 4461 Existence of the condition...
ifeqor 4462 The possible values of a c...
ifnot 4463 Negating the first argumen...
ifan 4464 Rewrite a conjunction in a...
ifor 4465 Rewrite a disjunction in a...
2if2 4466 Resolve two nested conditi...
ifcomnan 4467 Commute the conditions in ...
csbif 4468 Distribute proper substitu...
dedth 4469 Weak deduction theorem tha...
dedth2h 4470 Weak deduction theorem eli...
dedth3h 4471 Weak deduction theorem eli...
dedth4h 4472 Weak deduction theorem eli...
dedth2v 4473 Weak deduction theorem for...
dedth3v 4474 Weak deduction theorem for...
dedth4v 4475 Weak deduction theorem for...
elimhyp 4476 Eliminate a hypothesis con...
elimhyp2v 4477 Eliminate a hypothesis con...
elimhyp3v 4478 Eliminate a hypothesis con...
elimhyp4v 4479 Eliminate a hypothesis con...
elimel 4480 Eliminate a membership hyp...
elimdhyp 4481 Version of ~ elimhyp where...
keephyp 4482 Transform a hypothesis ` p...
keephyp2v 4483 Keep a hypothesis containi...
keephyp3v 4484 Keep a hypothesis containi...
pwjust 4486 Soundness justification th...
elpwg 4488 Membership in a power clas...
elpw 4489 Membership in a power clas...
velpw 4490 Setvar variable membership...
elpwOLD 4491 Obsolete proof of ~ elpw a...
elpwgOLD 4492 Obsolete proof of ~ elpwg ...
elpwd 4493 Membership in a power clas...
elpwi 4494 Subset relation implied by...
elpwb 4495 Characterization of the el...
elpwid 4496 An element of a power clas...
elelpwi 4497 If ` A ` belongs to a part...
sspw 4498 The powerclass preserves i...
sspwi 4499 The powerclass preserves i...
sspwd 4500 The powerclass preserves i...
pweq 4501 Equality theorem for power...
pweqALT 4502 Alternate proof of ~ pweq ...
pweqi 4503 Equality inference for pow...
pweqd 4504 Equality deduction for pow...
pwunss 4505 The power class of the uni...
nfpw 4506 Bound-variable hypothesis ...
pwidg 4507 A set is an element of its...
pwidb 4508 A class is an element of i...
pwid 4509 A set is a member of its p...
pwss 4510 Subclass relationship for ...
pwundif 4511 Break up the power class o...
snjust 4512 Soundness justification th...
sneq 4523 Equality theorem for singl...
sneqi 4524 Equality inference for sin...
sneqd 4525 Equality deduction for sin...
dfsn2 4526 Alternate definition of si...
elsng 4527 There is exactly one eleme...
elsn 4528 There is exactly one eleme...
velsn 4529 There is only one element ...
elsni 4530 There is at most one eleme...
absn 4531 Condition for a class abst...
dfpr2 4532 Alternate definition of a ...
dfsn2ALT 4533 Alternate definition of si...
elprg 4534 A member of a pair of clas...
elpri 4535 If a class is an element o...
elpr 4536 A member of a pair of clas...
elpr2g 4537 A member of a pair of sets...
elpr2 4538 A member of a pair of sets...
elpr2OLD 4539 Obsolete version of ~ elpr...
nelpr2 4540 If a class is not an eleme...
nelpr1 4541 If a class is not an eleme...
nelpri 4542 If an element doesn't matc...
prneli 4543 If an element doesn't matc...
nelprd 4544 If an element doesn't matc...
eldifpr 4545 Membership in a set with t...
rexdifpr 4546 Restricted existential qua...
snidg 4547 A set is a member of its s...
snidb 4548 A class is a set iff it is...
snid 4549 A set is a member of its s...
vsnid 4550 A setvar variable is a mem...
elsn2g 4551 There is exactly one eleme...
elsn2 4552 There is exactly one eleme...
nelsn 4553 If a class is not equal to...
rabeqsn 4554 Conditions for a restricte...
rabsssn 4555 Conditions for a restricte...
ralsnsg 4556 Substitution expressed in ...
rexsns 4557 Restricted existential qua...
rexsngf 4558 Restricted existential qua...
ralsngf 4559 Restricted universal quant...
reusngf 4560 Restricted existential uni...
ralsng 4561 Substitution expressed in ...
rexsng 4562 Restricted existential qua...
reusng 4563 Restricted existential uni...
2ralsng 4564 Substitution expressed in ...
ralsngOLD 4565 Obsolete version of ~ rals...
rexsngOLD 4566 Obsolete version of ~ rexs...
rexreusng 4567 Restricted existential uni...
exsnrex 4568 There is a set being the e...
ralsn 4569 Convert a universal quanti...
rexsn 4570 Convert an existential qua...
elpwunsn 4571 Membership in an extension...
eqoreldif 4572 An element of a set is eit...
eltpg 4573 Members of an unordered tr...
eldiftp 4574 Membership in a set with t...
eltpi 4575 A member of an unordered t...
eltp 4576 A member of an unordered t...
dftp2 4577 Alternate definition of un...
nfpr 4578 Bound-variable hypothesis ...
ifpr 4579 Membership of a conditiona...
ralprgf 4580 Convert a restricted unive...
rexprgf 4581 Convert a restricted exist...
ralprg 4582 Convert a restricted unive...
ralprgOLD 4583 Obsolete version of ~ ralp...
rexprg 4584 Convert a restricted exist...
rexprgOLD 4585 Obsolete version of ~ rexp...
raltpg 4586 Convert a restricted unive...
rextpg 4587 Convert a restricted exist...
ralpr 4588 Convert a restricted unive...
rexpr 4589 Convert a restricted exist...
reuprg0 4590 Convert a restricted exist...
reuprg 4591 Convert a restricted exist...
reurexprg 4592 Convert a restricted exist...
raltp 4593 Convert a universal quanti...
rextp 4594 Convert an existential qua...
nfsn 4595 Bound-variable hypothesis ...
csbsng 4596 Distribute proper substitu...
csbprg 4597 Distribute proper substitu...
elinsn 4598 If the intersection of two...
disjsn 4599 Intersection with the sing...
disjsn2 4600 Two distinct singletons ar...
disjpr2 4601 Two completely distinct un...
disjprsn 4602 The disjoint intersection ...
disjtpsn 4603 The disjoint intersection ...
disjtp2 4604 Two completely distinct un...
snprc 4605 The singleton of a proper ...
snnzb 4606 A singleton is nonempty if...
rmosn 4607 A restricted at-most-one q...
r19.12sn 4608 Special case of ~ r19.12 w...
rabsn 4609 Condition where a restrict...
rabsnifsb 4610 A restricted class abstrac...
rabsnif 4611 A restricted class abstrac...
rabrsn 4612 A restricted class abstrac...
euabsn2 4613 Another way to express exi...
euabsn 4614 Another way to express exi...
reusn 4615 A way to express restricte...
absneu 4616 Restricted existential uni...
rabsneu 4617 Restricted existential uni...
eusn 4618 Two ways to express " ` A ...
rabsnt 4619 Truth implied by equality ...
prcom 4620 Commutative law for unorde...
preq1 4621 Equality theorem for unord...
preq2 4622 Equality theorem for unord...
preq12 4623 Equality theorem for unord...
preq1i 4624 Equality inference for uno...
preq2i 4625 Equality inference for uno...
preq12i 4626 Equality inference for uno...
preq1d 4627 Equality deduction for uno...
preq2d 4628 Equality deduction for uno...
preq12d 4629 Equality deduction for uno...
tpeq1 4630 Equality theorem for unord...
tpeq2 4631 Equality theorem for unord...
tpeq3 4632 Equality theorem for unord...
tpeq1d 4633 Equality theorem for unord...
tpeq2d 4634 Equality theorem for unord...
tpeq3d 4635 Equality theorem for unord...
tpeq123d 4636 Equality theorem for unord...
tprot 4637 Rotation of the elements o...
tpcoma 4638 Swap 1st and 2nd members o...
tpcomb 4639 Swap 2nd and 3rd members o...
tpass 4640 Split off the first elemen...
qdass 4641 Two ways to write an unord...
qdassr 4642 Two ways to write an unord...
tpidm12 4643 Unordered triple ` { A , A...
tpidm13 4644 Unordered triple ` { A , B...
tpidm23 4645 Unordered triple ` { A , B...
tpidm 4646 Unordered triple ` { A , A...
tppreq3 4647 An unordered triple is an ...
prid1g 4648 An unordered pair contains...
prid2g 4649 An unordered pair contains...
prid1 4650 An unordered pair contains...
prid2 4651 An unordered pair contains...
ifpprsnss 4652 An unordered pair is a sin...
prprc1 4653 A proper class vanishes in...
prprc2 4654 A proper class vanishes in...
prprc 4655 An unordered pair containi...
tpid1 4656 One of the three elements ...
tpid1g 4657 Closed theorem form of ~ t...
tpid2 4658 One of the three elements ...
tpid2g 4659 Closed theorem form of ~ t...
tpid3g 4660 Closed theorem form of ~ t...
tpid3 4661 One of the three elements ...
snnzg 4662 The singleton of a set is ...
snn0d 4663 The singleton of a set is ...
snnz 4664 The singleton of a set is ...
prnz 4665 A pair containing a set is...
prnzg 4666 A pair containing a set is...
tpnz 4667 An unordered triple contai...
tpnzd 4668 An unordered triple contai...
raltpd 4669 Convert a universal quanti...
snssg 4670 The singleton of an elemen...
snss 4671 The singleton of an elemen...
eldifsn 4672 Membership in a set with a...
ssdifsn 4673 Subset of a set with an el...
elpwdifsn 4674 A subset of a set is an el...
eldifsni 4675 Membership in a set with a...
eldifsnneq 4676 An element of a difference...
neldifsn 4677 The class ` A ` is not in ...
neldifsnd 4678 The class ` A ` is not in ...
rexdifsn 4679 Restricted existential qua...
raldifsni 4680 Rearrangement of a propert...
raldifsnb 4681 Restricted universal quant...
eldifvsn 4682 A set is an element of the...
difsn 4683 An element not in a set ca...
difprsnss 4684 Removal of a singleton fro...
difprsn1 4685 Removal of a singleton fro...
difprsn2 4686 Removal of a singleton fro...
diftpsn3 4687 Removal of a singleton fro...
difpr 4688 Removing two elements as p...
tpprceq3 4689 An unordered triple is an ...
tppreqb 4690 An unordered triple is an ...
difsnb 4691 ` ( B \ { A } ) ` equals `...
difsnpss 4692 ` ( B \ { A } ) ` is a pro...
snssi 4693 The singleton of an elemen...
snssd 4694 The singleton of an elemen...
difsnid 4695 If we remove a single elem...
eldifeldifsn 4696 An element of a difference...
pw0 4697 Compute the power set of t...
pwpw0 4698 Compute the power set of t...
snsspr1 4699 A singleton is a subset of...
snsspr2 4700 A singleton is a subset of...
snsstp1 4701 A singleton is a subset of...
snsstp2 4702 A singleton is a subset of...
snsstp3 4703 A singleton is a subset of...
prssg 4704 A pair of elements of a cl...
prss 4705 A pair of elements of a cl...
prssi 4706 A pair of elements of a cl...
prssd 4707 Deduction version of ~ prs...
prsspwg 4708 An unordered pair belongs ...
ssprss 4709 A pair as subset of a pair...
ssprsseq 4710 A proper pair is a subset ...
sssn 4711 The subsets of a singleton...
ssunsn2 4712 The property of being sand...
ssunsn 4713 Possible values for a set ...
eqsn 4714 Two ways to express that a...
issn 4715 A sufficient condition for...
n0snor2el 4716 A nonempty set is either a...
ssunpr 4717 Possible values for a set ...
sspr 4718 The subsets of a pair. (C...
sstp 4719 The subsets of an unordere...
tpss 4720 An unordered triple of ele...
tpssi 4721 An unordered triple of ele...
sneqrg 4722 Closed form of ~ sneqr . ...
sneqr 4723 If the singletons of two s...
snsssn 4724 If a singleton is a subset...
mosneq 4725 There exists at most one s...
sneqbg 4726 Two singletons of sets are...
snsspw 4727 The singleton of a class i...
prsspw 4728 An unordered pair belongs ...
preq1b 4729 Biconditional equality lem...
preq2b 4730 Biconditional equality lem...
preqr1 4731 Reverse equality lemma for...
preqr2 4732 Reverse equality lemma for...
preq12b 4733 Equality relationship for ...
opthpr 4734 An unordered pair has the ...
preqr1g 4735 Reverse equality lemma for...
preq12bg 4736 Closed form of ~ preq12b ....
prneimg 4737 Two pairs are not equal if...
prnebg 4738 A (proper) pair is not equ...
pr1eqbg 4739 A (proper) pair is equal t...
pr1nebg 4740 A (proper) pair is not equ...
preqsnd 4741 Equivalence for a pair equ...
prnesn 4742 A proper unordered pair is...
prneprprc 4743 A proper unordered pair is...
preqsn 4744 Equivalence for a pair equ...
preq12nebg 4745 Equality relationship for ...
prel12g 4746 Equality of two unordered ...
opthprneg 4747 An unordered pair has the ...
elpreqprlem 4748 Lemma for ~ elpreqpr . (C...
elpreqpr 4749 Equality and membership ru...
elpreqprb 4750 A set is an element of an ...
elpr2elpr 4751 For an element ` A ` of an...
dfopif 4752 Rewrite ~ df-op using ` if...
dfopifOLD 4753 Obsolete version of ~ dfop...
dfopg 4754 Value of the ordered pair ...
dfop 4755 Value of an ordered pair w...
opeq1 4756 Equality theorem for order...
opeq1OLD 4757 Obsolete version of ~ opeq...
opeq2 4758 Equality theorem for order...
opeq2OLD 4759 Obsolete version of ~ opeq...
opeq12 4760 Equality theorem for order...
opeq1i 4761 Equality inference for ord...
opeq2i 4762 Equality inference for ord...
opeq12i 4763 Equality inference for ord...
opeq1d 4764 Equality deduction for ord...
opeq2d 4765 Equality deduction for ord...
opeq12d 4766 Equality deduction for ord...
oteq1 4767 Equality theorem for order...
oteq2 4768 Equality theorem for order...
oteq3 4769 Equality theorem for order...
oteq1d 4770 Equality deduction for ord...
oteq2d 4771 Equality deduction for ord...
oteq3d 4772 Equality deduction for ord...
oteq123d 4773 Equality deduction for ord...
nfop 4774 Bound-variable hypothesis ...
nfopd 4775 Deduction version of bound...
csbopg 4776 Distribution of class subs...
opidg 4777 The ordered pair ` <. A , ...
opid 4778 The ordered pair ` <. A , ...
ralunsn 4779 Restricted quantification ...
2ralunsn 4780 Double restricted quantifi...
opprc 4781 Expansion of an ordered pa...
opprc1 4782 Expansion of an ordered pa...
opprc2 4783 Expansion of an ordered pa...
oprcl 4784 If an ordered pair has an ...
pwsn 4785 The power set of a singlet...
pwsnOLD 4786 Obsolete version of ~ pwsn...
pwpr 4787 The power set of an unorde...
pwtp 4788 The power set of an unorde...
pwpwpw0 4789 Compute the power set of t...
pwv 4790 The power class of the uni...
prproe 4791 For an element of a proper...
3elpr2eq 4792 If there are three element...
dfuni2 4795 Alternate definition of cl...
eluni 4796 Membership in class union....
eluni2 4797 Membership in class union....
elunii 4798 Membership in class union....
nfunid 4799 Deduction version of ~ nfu...
nfuni 4800 Bound-variable hypothesis ...
uniss 4801 Subclass relationship for ...
unissi 4802 Subclass relationship for ...
unissd 4803 Subclass relationship for ...
unieq 4804 Equality theorem for class...
unieqOLD 4805 Obsolete version of ~ unie...
unieqi 4806 Inference of equality of t...
unieqd 4807 Deduction of equality of t...
eluniab 4808 Membership in union of a c...
elunirab 4809 Membership in union of a c...
uniprg 4810 The union of a pair is the...
unipr 4811 The union of a pair is the...
uniprOLD 4812 Obsolete version of ~ unip...
uniprgOLD 4813 Obsolete version of ~ unip...
unisng 4814 A set equals the union of ...
unisn 4815 A set equals the union of ...
unisn3 4816 Union of a singleton in th...
dfnfc2 4817 An alternative statement o...
uniun 4818 The class union of the uni...
uniin 4819 The class union of the int...
ssuni 4820 Subclass relationship for ...
uni0b 4821 The union of a set is empt...
uni0c 4822 The union of a set is empt...
uni0 4823 The union of the empty set...
csbuni 4824 Distribute proper substitu...
elssuni 4825 An element of a class is a...
unissel 4826 Condition turning a subcla...
unissb 4827 Relationship involving mem...
uniss2 4828 A subclass condition on th...
unidif 4829 If the difference ` A \ B ...
ssunieq 4830 Relationship implying unio...
unimax 4831 Any member of a class is t...
pwuni 4832 A class is a subclass of t...
dfint2 4835 Alternate definition of cl...
inteq 4836 Equality law for intersect...
inteqi 4837 Equality inference for cla...
inteqd 4838 Equality deduction for cla...
elint 4839 Membership in class inters...
elint2 4840 Membership in class inters...
elintg 4841 Membership in class inters...
elinti 4842 Membership in class inters...
nfint 4843 Bound-variable hypothesis ...
elintab 4844 Membership in the intersec...
elintrab 4845 Membership in the intersec...
elintrabg 4846 Membership in the intersec...
int0 4847 The intersection of the em...
intss1 4848 An element of a class incl...
ssint 4849 Subclass of a class inters...
ssintab 4850 Subclass of the intersecti...
ssintub 4851 Subclass of the least uppe...
ssmin 4852 Subclass of the minimum va...
intmin 4853 Any member of a class is t...
intss 4854 Intersection of subclasses...
intssuni 4855 The intersection of a none...
ssintrab 4856 Subclass of the intersecti...
unissint 4857 If the union of a class is...
intssuni2 4858 Subclass relationship for ...
intminss 4859 Under subset ordering, the...
intmin2 4860 Any set is the smallest of...
intmin3 4861 Under subset ordering, the...
intmin4 4862 Elimination of a conjunct ...
intab 4863 The intersection of a spec...
int0el 4864 The intersection of a clas...
intun 4865 The class intersection of ...
intprg 4866 The intersection of a pair...
intpr 4867 The intersection of a pair...
intprOLD 4868 Obsolete version of ~ intp...
intprgOLD 4869 Obsolete version of ~ intp...
intsng 4870 Intersection of a singleto...
intsn 4871 The intersection of a sing...
uniintsn 4872 Two ways to express " ` A ...
uniintab 4873 The union and the intersec...
intunsn 4874 Theorem joining a singleto...
rint0 4875 Relative intersection of a...
elrint 4876 Membership in a restricted...
elrint2 4877 Membership in a restricted...
eliun 4882 Membership in indexed unio...
eliin 4883 Membership in indexed inte...
eliuni 4884 Membership in an indexed u...
iuncom 4885 Commutation of indexed uni...
iuncom4 4886 Commutation of union with ...
iunconst 4887 Indexed union of a constan...
iinconst 4888 Indexed intersection of a ...
iuneqconst 4889 Indexed union of identical...
iuniin 4890 Law combining indexed unio...
iinssiun 4891 An indexed intersection is...
iunss1 4892 Subclass theorem for index...
iinss1 4893 Subclass theorem for index...
iuneq1 4894 Equality theorem for index...
iineq1 4895 Equality theorem for index...
ss2iun 4896 Subclass theorem for index...
iuneq2 4897 Equality theorem for index...
iineq2 4898 Equality theorem for index...
iuneq2i 4899 Equality inference for ind...
iineq2i 4900 Equality inference for ind...
iineq2d 4901 Equality deduction for ind...
iuneq2dv 4902 Equality deduction for ind...
iineq2dv 4903 Equality deduction for ind...
iuneq12df 4904 Equality deduction for ind...
iuneq1d 4905 Equality theorem for index...
iuneq12d 4906 Equality deduction for ind...
iuneq2d 4907 Equality deduction for ind...
nfiun 4908 Bound-variable hypothesis ...
nfiin 4909 Bound-variable hypothesis ...
nfiung 4910 Bound-variable hypothesis ...
nfiing 4911 Bound-variable hypothesis ...
nfiu1 4912 Bound-variable hypothesis ...
nfii1 4913 Bound-variable hypothesis ...
dfiun2g 4914 Alternate definition of in...
dfiin2g 4915 Alternate definition of in...
dfiun2 4916 Alternate definition of in...
dfiin2 4917 Alternate definition of in...
dfiunv2 4918 Define double indexed unio...
cbviun 4919 Rule used to change the bo...
cbviin 4920 Change bound variables in ...
cbviung 4921 Rule used to change the bo...
cbviing 4922 Change bound variables in ...
cbviunv 4923 Rule used to change the bo...
cbviinv 4924 Change bound variables in ...
cbviunvg 4925 Rule used to change the bo...
cbviinvg 4926 Change bound variables in ...
iunssf 4927 Subset theorem for an inde...
iunss 4928 Subset theorem for an inde...
ssiun 4929 Subset implication for an ...
ssiun2 4930 Identity law for subset of...
ssiun2s 4931 Subset relationship for an...
iunss2 4932 A subclass condition on th...
iunssd 4933 Subset theorem for an inde...
iunab 4934 The indexed union of a cla...
iunrab 4935 The indexed union of a res...
iunxdif2 4936 Indexed union with a class...
ssiinf 4937 Subset theorem for an inde...
ssiin 4938 Subset theorem for an inde...
iinss 4939 Subset implication for an ...
iinss2 4940 An indexed intersection is...
uniiun 4941 Class union in terms of in...
intiin 4942 Class intersection in term...
iunid 4943 An indexed union of single...
iun0 4944 An indexed union of the em...
0iun 4945 An empty indexed union is ...
0iin 4946 An empty indexed intersect...
viin 4947 Indexed intersection with ...
iunsn 4948 Indexed union of a singlet...
iunn0 4949 There is a nonempty class ...
iinab 4950 Indexed intersection of a ...
iinrab 4951 Indexed intersection of a ...
iinrab2 4952 Indexed intersection of a ...
iunin2 4953 Indexed union of intersect...
iunin1 4954 Indexed union of intersect...
iinun2 4955 Indexed intersection of un...
iundif2 4956 Indexed union of class dif...
iindif1 4957 Indexed intersection of cl...
2iunin 4958 Rearrange indexed unions o...
iindif2 4959 Indexed intersection of cl...
iinin2 4960 Indexed intersection of in...
iinin1 4961 Indexed intersection of in...
iinvdif 4962 The indexed intersection o...
elriin 4963 Elementhood in a relative ...
riin0 4964 Relative intersection of a...
riinn0 4965 Relative intersection of a...
riinrab 4966 Relative intersection of a...
symdif0 4967 Symmetric difference with ...
symdifv 4968 The symmetric difference w...
symdifid 4969 The symmetric difference o...
iinxsng 4970 A singleton index picks ou...
iinxprg 4971 Indexed intersection with ...
iunxsng 4972 A singleton index picks ou...
iunxsn 4973 A singleton index picks ou...
iunxsngf 4974 A singleton index picks ou...
iunun 4975 Separate a union in an ind...
iunxun 4976 Separate a union in the in...
iunxdif3 4977 An indexed union where som...
iunxprg 4978 A pair index picks out two...
iunxiun 4979 Separate an indexed union ...
iinuni 4980 A relationship involving u...
iununi 4981 A relationship involving u...
sspwuni 4982 Subclass relationship for ...
pwssb 4983 Two ways to express a coll...
elpwpw 4984 Characterization of the el...
pwpwab 4985 The double power class wri...
pwpwssunieq 4986 The class of sets whose un...
elpwuni 4987 Relationship for power cla...
iinpw 4988 The power class of an inte...
iunpwss 4989 Inclusion of an indexed un...
intss2 4990 A nonempty intersection of...
rintn0 4991 Relative intersection of a...
dfdisj2 4994 Alternate definition for d...
disjss2 4995 If each element of a colle...
disjeq2 4996 Equality theorem for disjo...
disjeq2dv 4997 Equality deduction for dis...
disjss1 4998 A subset of a disjoint col...
disjeq1 4999 Equality theorem for disjo...
disjeq1d 5000 Equality theorem for disjo...
disjeq12d 5001 Equality theorem for disjo...
cbvdisj 5002 Change bound variables in ...
cbvdisjv 5003 Change bound variables in ...
nfdisjw 5004 Bound-variable hypothesis ...
nfdisj 5005 Bound-variable hypothesis ...
nfdisj1 5006 Bound-variable hypothesis ...
disjor 5007 Two ways to say that a col...
disjors 5008 Two ways to say that a col...
disji2 5009 Property of a disjoint col...
disji 5010 Property of a disjoint col...
invdisj 5011 If there is a function ` C...
invdisjrabw 5012 Version of ~ invdisjrab wi...
invdisjrab 5013 The restricted class abstr...
disjiun 5014 A disjoint collection yiel...
disjord 5015 Conditions for a collectio...
disjiunb 5016 Two ways to say that a col...
disjiund 5017 Conditions for a collectio...
sndisj 5018 Any collection of singleto...
0disj 5019 Any collection of empty se...
disjxsn 5020 A singleton collection is ...
disjx0 5021 An empty collection is dis...
disjprgw 5022 Version of ~ disjprg with ...
disjprg 5023 A pair collection is disjo...
disjxiun 5024 An indexed union of a disj...
disjxun 5025 The union of two disjoint ...
disjss3 5026 Expand a disjoint collecti...
breq 5029 Equality theorem for binar...
breq1 5030 Equality theorem for a bin...
breq2 5031 Equality theorem for a bin...
breq12 5032 Equality theorem for a bin...
breqi 5033 Equality inference for bin...
breq1i 5034 Equality inference for a b...
breq2i 5035 Equality inference for a b...
breq12i 5036 Equality inference for a b...
breq1d 5037 Equality deduction for a b...
breqd 5038 Equality deduction for a b...
breq2d 5039 Equality deduction for a b...
breq12d 5040 Equality deduction for a b...
breq123d 5041 Equality deduction for a b...
breqdi 5042 Equality deduction for a b...
breqan12d 5043 Equality deduction for a b...
breqan12rd 5044 Equality deduction for a b...
eqnbrtrd 5045 Substitution of equal clas...
nbrne1 5046 Two classes are different ...
nbrne2 5047 Two classes are different ...
eqbrtri 5048 Substitution of equal clas...
eqbrtrd 5049 Substitution of equal clas...
eqbrtrri 5050 Substitution of equal clas...
eqbrtrrd 5051 Substitution of equal clas...
breqtri 5052 Substitution of equal clas...
breqtrd 5053 Substitution of equal clas...
breqtrri 5054 Substitution of equal clas...
breqtrrd 5055 Substitution of equal clas...
3brtr3i 5056 Substitution of equality i...
3brtr4i 5057 Substitution of equality i...
3brtr3d 5058 Substitution of equality i...
3brtr4d 5059 Substitution of equality i...
3brtr3g 5060 Substitution of equality i...
3brtr4g 5061 Substitution of equality i...
eqbrtrid 5062 A chained equality inferen...
eqbrtrrid 5063 A chained equality inferen...
breqtrid 5064 A chained equality inferen...
breqtrrid 5065 A chained equality inferen...
eqbrtrdi 5066 A chained equality inferen...
eqbrtrrdi 5067 A chained equality inferen...
breqtrdi 5068 A chained equality inferen...
breqtrrdi 5069 A chained equality inferen...
ssbrd 5070 Deduction from a subclass ...
ssbr 5071 Implication from a subclas...
ssbri 5072 Inference from a subclass ...
nfbrd 5073 Deduction version of bound...
nfbr 5074 Bound-variable hypothesis ...
brab1 5075 Relationship between a bin...
br0 5076 The empty binary relation ...
brne0 5077 If two sets are in a binar...
brun 5078 The union of two binary re...
brin 5079 The intersection of two re...
brdif 5080 The difference of two bina...
sbcbr123 5081 Move substitution in and o...
sbcbr 5082 Move substitution in and o...
sbcbr12g 5083 Move substitution in and o...
sbcbr1g 5084 Move substitution in and o...
sbcbr2g 5085 Move substitution in and o...
brsymdif 5086 Characterization of the sy...
brralrspcev 5087 Restricted existential spe...
brimralrspcev 5088 Restricted existential spe...
opabss 5091 The collection of ordered ...
opabbid 5092 Equivalent wff's yield equ...
opabbidv 5093 Equivalent wff's yield equ...
opabbii 5094 Equivalent wff's yield equ...
nfopab 5095 Bound-variable hypothesis ...
nfopab1 5096 The first abstraction vari...
nfopab2 5097 The second abstraction var...
cbvopab 5098 Rule used to change bound ...
cbvopabv 5099 Rule used to change bound ...
cbvopab1 5100 Change first bound variabl...
cbvopab1g 5101 Change first bound variabl...
cbvopab2 5102 Change second bound variab...
cbvopab1s 5103 Change first bound variabl...
cbvopab1v 5104 Rule used to change the fi...
cbvopab2v 5105 Rule used to change the se...
unopab 5106 Union of two ordered pair ...
mpteq12df 5109 An equality inference for ...
mpteq12f 5110 An equality theorem for th...
mpteq12dva 5111 An equality inference for ...
mpteq12dv 5112 An equality inference for ...
mpteq12dvOLD 5113 Obsolete version of ~ mpte...
mpteq12 5114 An equality theorem for th...
mpteq1 5115 An equality theorem for th...
mpteq1d 5116 An equality theorem for th...
mpteq1i 5117 An equality theorem for th...
mpteq2ia 5118 An equality inference for ...
mpteq2i 5119 An equality inference for ...
mpteq12i 5120 An equality inference for ...
mpteq2da 5121 Slightly more general equa...
mpteq2dva 5122 Slightly more general equa...
mpteq2dv 5123 An equality inference for ...
nfmpt 5124 Bound-variable hypothesis ...
nfmpt1 5125 Bound-variable hypothesis ...
cbvmptf 5126 Rule to change the bound v...
cbvmptfg 5127 Rule to change the bound v...
cbvmpt 5128 Rule to change the bound v...
cbvmptg 5129 Rule to change the bound v...
cbvmptv 5130 Rule to change the bound v...
cbvmptvg 5131 Rule to change the bound v...
mptv 5132 Function with universal do...
dftr2 5135 An alternate way of defini...
dftr5 5136 An alternate way of defini...
dftr3 5137 An alternate way of defini...
dftr4 5138 An alternate way of defini...
treq 5139 Equality theorem for the t...
trel 5140 In a transitive class, the...
trel3 5141 In a transitive class, the...
trss 5142 An element of a transitive...
trin 5143 The intersection of transi...
tr0 5144 The empty set is transitiv...
trv 5145 The universe is transitive...
triun 5146 An indexed union of a clas...
truni 5147 The union of a class of tr...
triin 5148 An indexed intersection of...
trint 5149 The intersection of a clas...
trintss 5150 Any nonempty transitive cl...
axrep1 5152 The version of the Axiom o...
axreplem 5153 Lemma for ~ axrep2 and ~ a...
axrep2 5154 Axiom of Replacement expre...
axrep3 5155 Axiom of Replacement sligh...
axrep4 5156 A more traditional version...
axrep5 5157 Axiom of Replacement (simi...
axrep6 5158 A condensed form of ~ ax-r...
zfrepclf 5159 An inference based on the ...
zfrep3cl 5160 An inference based on the ...
zfrep4 5161 A version of Replacement u...
axsepgfromrep 5162 A more general version ~ a...
axsep 5163 Axiom scheme of separation...
axsepg 5165 A more general version of ...
zfauscl 5166 Separation Scheme (Aussond...
bm1.3ii 5167 Convert implication to equ...
ax6vsep 5168 Derive ~ ax6v (a weakened ...
axnulALT 5169 Alternate proof of ~ axnul...
axnul 5170 The Null Set Axiom of ZF s...
0ex 5172 The Null Set Axiom of ZF s...
al0ssb 5173 The empty set is the uniqu...
sseliALT 5174 Alternate proof of ~ sseli...
csbexg 5175 The existence of proper su...
csbex 5176 The existence of proper su...
unisn2 5177 A version of ~ unisn witho...
nalset 5178 No set contains all sets. ...
vnex 5179 The universal class does n...
vprc 5180 The universal class is not...
nvel 5181 The universal class does n...
inex1 5182 Separation Scheme (Aussond...
inex2 5183 Separation Scheme (Aussond...
inex1g 5184 Closed-form, generalized S...
inex2g 5185 Sufficient condition for a...
ssex 5186 The subset of a set is als...
ssexi 5187 The subset of a set is als...
ssexg 5188 The subset of a set is als...
ssexd 5189 A subclass of a set is a s...
prcssprc 5190 The superclass of a proper...
sselpwd 5191 Elementhood to a power set...
difexg 5192 Existence of a difference....
difexi 5193 Existence of a difference,...
difexd 5194 Existence of a difference....
zfausab 5195 Separation Scheme (Aussond...
rabexg 5196 Separation Scheme in terms...
rabex 5197 Separation Scheme in terms...
rabexd 5198 Separation Scheme in terms...
rabex2 5199 Separation Scheme in terms...
rab2ex 5200 A class abstraction based ...
elssabg 5201 Membership in a class abst...
intex 5202 The intersection of a none...
intnex 5203 If a class intersection is...
intexab 5204 The intersection of a none...
intexrab 5205 The intersection of a none...
iinexg 5206 The existence of a class i...
intabs 5207 Absorption of a redundant ...
inuni 5208 The intersection of a unio...
elpw2g 5209 Membership in a power clas...
elpw2 5210 Membership in a power clas...
elpwi2 5211 Membership in a power clas...
elpwi2OLD 5212 Obsolete version of ~ elpw...
pwnss 5213 The power set of a set is ...
pwne 5214 No set equals its power se...
difelpw 5215 A difference is an element...
rabelpw 5216 A restricted class abstrac...
class2set 5217 Construct, from any class ...
class2seteq 5218 Equality theorem based on ...
0elpw 5219 Every power class contains...
pwne0 5220 A power class is never emp...
0nep0 5221 The empty set and its powe...
0inp0 5222 Something cannot be equal ...
unidif0 5223 The removal of the empty s...
iin0 5224 An indexed intersection of...
notzfaus 5225 In the Separation Scheme ~...
notzfausOLD 5226 Obsolete proof of ~ notzfa...
intv 5227 The intersection of the un...
axpweq 5228 Two equivalent ways to exp...
zfpow 5230 Axiom of Power Sets expres...
axpow2 5231 A variant of the Axiom of ...
axpow3 5232 A variant of the Axiom of ...
el 5233 Every set is an element of...
dtru 5234 At least two sets exist (o...
dtrucor 5235 Corollary of ~ dtru . Thi...
dtrucor2 5236 The theorem form of the de...
dvdemo1 5237 Demonstration of a theorem...
dvdemo2 5238 Demonstration of a theorem...
nfnid 5239 A setvar variable is not f...
nfcvb 5240 The "distinctor" expressio...
vpwex 5241 Power set axiom: the power...
pwexg 5242 Power set axiom expressed ...
pwexd 5243 Deduction version of the p...
pwex 5244 Power set axiom expressed ...
pwel 5245 Quantitative version of ~ ...
abssexg 5246 Existence of a class of su...
snexALT 5247 Alternate proof of ~ snex ...
p0ex 5248 The power set of the empty...
p0exALT 5249 Alternate proof of ~ p0ex ...
pp0ex 5250 The power set of the power...
ord3ex 5251 The ordinal number 3 is a ...
dtruALT 5252 Alternate proof of ~ dtru ...
axc16b 5253 This theorem shows that Ax...
eunex 5254 Existential uniqueness imp...
eusv1 5255 Two ways to express single...
eusvnf 5256 Even if ` x ` is free in `...
eusvnfb 5257 Two ways to say that ` A (...
eusv2i 5258 Two ways to express single...
eusv2nf 5259 Two ways to express single...
eusv2 5260 Two ways to express single...
reusv1 5261 Two ways to express single...
reusv2lem1 5262 Lemma for ~ reusv2 . (Con...
reusv2lem2 5263 Lemma for ~ reusv2 . (Con...
reusv2lem3 5264 Lemma for ~ reusv2 . (Con...
reusv2lem4 5265 Lemma for ~ reusv2 . (Con...
reusv2lem5 5266 Lemma for ~ reusv2 . (Con...
reusv2 5267 Two ways to express single...
reusv3i 5268 Two ways of expressing exi...
reusv3 5269 Two ways to express single...
eusv4 5270 Two ways to express single...
alxfr 5271 Transfer universal quantif...
ralxfrd 5272 Transfer universal quantif...
rexxfrd 5273 Transfer universal quantif...
ralxfr2d 5274 Transfer universal quantif...
rexxfr2d 5275 Transfer universal quantif...
ralxfrd2 5276 Transfer universal quantif...
rexxfrd2 5277 Transfer existence from a ...
ralxfr 5278 Transfer universal quantif...
ralxfrALT 5279 Alternate proof of ~ ralxf...
rexxfr 5280 Transfer existence from a ...
rabxfrd 5281 Membership in a restricted...
rabxfr 5282 Membership in a restricted...
reuhypd 5283 A theorem useful for elimi...
reuhyp 5284 A theorem useful for elimi...
zfpair 5285 The Axiom of Pairing of Ze...
axprALT 5286 Alternate proof of ~ axpr ...
axprlem1 5287 Lemma for ~ axpr . There ...
axprlem2 5288 Lemma for ~ axpr . There ...
axprlem3 5289 Lemma for ~ axpr . Elimin...
axprlem4 5290 Lemma for ~ axpr . The fi...
axprlem5 5291 Lemma for ~ axpr . The se...
axpr 5292 Unabbreviated version of t...
zfpair2 5294 Derive the abbreviated ver...
snex 5295 A singleton is a set. The...
prex 5296 The Axiom of Pairing using...
sels 5297 If a class is a set, then ...
elALT 5298 Alternate proof of ~ el , ...
dtruALT2 5299 Alternate proof of ~ dtru ...
snelpwi 5300 A singleton of a set belon...
snelpw 5301 A singleton of a set belon...
prelpw 5302 A pair of two sets belongs...
prelpwi 5303 A pair of two sets belongs...
rext 5304 A theorem similar to exten...
sspwb 5305 The powerclass constructio...
unipw 5306 A class equals the union o...
univ 5307 The union of the universe ...
pwtr 5308 A class is transitive iff ...
ssextss 5309 An extensionality-like pri...
ssext 5310 An extensionality-like pri...
nssss 5311 Negation of subclass relat...
pweqb 5312 Classes are equal if and o...
intid 5313 The intersection of all se...
moabex 5314 "At most one" existence im...
rmorabex 5315 Restricted "at most one" e...
euabex 5316 The abstraction of a wff w...
nnullss 5317 A nonempty class (even if ...
exss 5318 Restricted existence in a ...
opex 5319 An ordered pair of classes...
otex 5320 An ordered triple of class...
elopg 5321 Characterization of the el...
elop 5322 Characterization of the el...
opi1 5323 One of the two elements in...
opi2 5324 One of the two elements of...
opeluu 5325 Each member of an ordered ...
op1stb 5326 Extract the first member o...
brv 5327 Two classes are always in ...
opnz 5328 An ordered pair is nonempt...
opnzi 5329 An ordered pair is nonempt...
opth1 5330 Equality of the first memb...
opth 5331 The ordered pair theorem. ...
opthg 5332 Ordered pair theorem. ` C ...
opth1g 5333 Equality of the first memb...
opthg2 5334 Ordered pair theorem. (Co...
opth2 5335 Ordered pair theorem. (Co...
opthneg 5336 Two ordered pairs are not ...
opthne 5337 Two ordered pairs are not ...
otth2 5338 Ordered triple theorem, wi...
otth 5339 Ordered triple theorem. (...
otthg 5340 Ordered triple theorem, cl...
eqvinop 5341 A variable introduction la...
sbcop1 5342 The proper substitution of...
sbcop 5343 The proper substitution of...
copsexgw 5344 Version of ~ copsexg with ...
copsexg 5345 Substitution of class ` A ...
copsex2t 5346 Closed theorem form of ~ c...
copsex2g 5347 Implicit substitution infe...
copsex2gOLD 5348 Obsolete version of ~ cops...
copsex4g 5349 An implicit substitution i...
0nelop 5350 A property of ordered pair...
opwo0id 5351 An ordered pair is equal t...
opeqex 5352 Equivalence of existence i...
oteqex2 5353 Equivalence of existence i...
oteqex 5354 Equivalence of existence i...
opcom 5355 An ordered pair commutes i...
moop2 5356 "At most one" property of ...
opeqsng 5357 Equivalence for an ordered...
opeqsn 5358 Equivalence for an ordered...
opeqpr 5359 Equivalence for an ordered...
snopeqop 5360 Equivalence for an ordered...
propeqop 5361 Equivalence for an ordered...
propssopi 5362 If a pair of ordered pairs...
snopeqopsnid 5363 Equivalence for an ordered...
mosubopt 5364 "At most one" remains true...
mosubop 5365 "At most one" remains true...
euop2 5366 Transfer existential uniqu...
euotd 5367 Prove existential uniquene...
opthwiener 5368 Justification theorem for ...
uniop 5369 The union of an ordered pa...
uniopel 5370 Ordered pair membership is...
opthhausdorff 5371 Justification theorem for ...
opthhausdorff0 5372 Justification theorem for ...
otsndisj 5373 The singletons consisting ...
otiunsndisj 5374 The union of singletons co...
iunopeqop 5375 Implication of an ordered ...
brsnop 5376 Binary relation for an ord...
opabidw 5377 The law of concretion. Sp...
opabid 5378 The law of concretion. Sp...
elopab 5379 Membership in a class abst...
rexopabb 5380 Restricted existential qua...
vopelopabsb 5381 The law of concretion in t...
opelopabsb 5382 The law of concretion in t...
brabsb 5383 The law of concretion in t...
opelopabt 5384 Closed theorem form of ~ o...
opelopabga 5385 The law of concretion. Th...
brabga 5386 The law of concretion for ...
opelopab2a 5387 Ordered pair membership in...
opelopaba 5388 The law of concretion. Th...
braba 5389 The law of concretion for ...
opelopabg 5390 The law of concretion. Th...
brabg 5391 The law of concretion for ...
opelopabgf 5392 The law of concretion. Th...
opelopab2 5393 Ordered pair membership in...
opelopab 5394 The law of concretion. Th...
brab 5395 The law of concretion for ...
opelopabaf 5396 The law of concretion. Th...
opelopabf 5397 The law of concretion. Th...
ssopab2 5398 Equivalence of ordered pai...
ssopab2bw 5399 Equivalence of ordered pai...
eqopab2bw 5400 Equivalence of ordered pai...
ssopab2b 5401 Equivalence of ordered pai...
ssopab2i 5402 Inference of ordered pair ...
ssopab2dv 5403 Inference of ordered pair ...
eqopab2b 5404 Equivalence of ordered pai...
opabn0 5405 Nonempty ordered pair clas...
opab0 5406 Empty ordered pair class a...
csbopab 5407 Move substitution into a c...
csbopabgALT 5408 Move substitution into a c...
csbmpt12 5409 Move substitution into a m...
csbmpt2 5410 Move substitution into the...
iunopab 5411 Move indexed union inside ...
elopabr 5412 Membership in an ordered-p...
elopabran 5413 Membership in an ordered-p...
rbropapd 5414 Properties of a pair in an...
rbropap 5415 Properties of a pair in a ...
2rbropap 5416 Properties of a pair in a ...
0nelopab 5417 The empty set is never an ...
brabv 5418 If two classes are in a re...
pwin 5419 The power class of the int...
pwunssOLD 5420 Obsolete version of ~ pwun...
pwssun 5421 The power class of the uni...
pwundifOLD 5422 Obsolete proof of ~ pwundi...
pwun 5423 The power class of the uni...
dfid4 5426 The identity function expr...
dfid3 5427 A stronger version of ~ df...
dfid2 5428 Alternate definition of th...
epelg 5431 The membership relation an...
epeli 5432 The membership relation an...
epel 5433 The membership relation an...
0sn0ep 5434 An example for the members...
epn0 5435 The membership relation is...
poss 5440 Subset theorem for the par...
poeq1 5441 Equality theorem for parti...
poeq2 5442 Equality theorem for parti...
nfpo 5443 Bound-variable hypothesis ...
nfso 5444 Bound-variable hypothesis ...
pocl 5445 Properties of partial orde...
ispod 5446 Sufficient conditions for ...
swopolem 5447 Perform the substitutions ...
swopo 5448 A strict weak order is a p...
poirr 5449 A partial order relation i...
potr 5450 A partial order relation i...
po2nr 5451 A partial order relation h...
po3nr 5452 A partial order relation h...
po2ne 5453 Two classes which are in a...
po0 5454 Any relation is a partial ...
pofun 5455 A function preserves a par...
sopo 5456 A strict linear order is a...
soss 5457 Subset theorem for the str...
soeq1 5458 Equality theorem for the s...
soeq2 5459 Equality theorem for the s...
sonr 5460 A strict order relation is...
sotr 5461 A strict order relation is...
solin 5462 A strict order relation is...
so2nr 5463 A strict order relation ha...
so3nr 5464 A strict order relation ha...
sotric 5465 A strict order relation sa...
sotrieq 5466 Trichotomy law for strict ...
sotrieq2 5467 Trichotomy law for strict ...
soasym 5468 Asymmetry law for strict o...
sotr2 5469 A transitivity relation. ...
issod 5470 An irreflexive, transitive...
issoi 5471 An irreflexive, transitive...
isso2i 5472 Deduce strict ordering fro...
so0 5473 Any relation is a strict o...
somo 5474 A totally ordered set has ...
fri 5481 Property of well-founded r...
seex 5482 The ` R ` -preimage of an ...
exse 5483 Any relation on a set is s...
dffr2 5484 Alternate definition of we...
frc 5485 Property of well-founded r...
frss 5486 Subset theorem for the wel...
sess1 5487 Subset theorem for the set...
sess2 5488 Subset theorem for the set...
freq1 5489 Equality theorem for the w...
freq2 5490 Equality theorem for the w...
seeq1 5491 Equality theorem for the s...
seeq2 5492 Equality theorem for the s...
nffr 5493 Bound-variable hypothesis ...
nfse 5494 Bound-variable hypothesis ...
nfwe 5495 Bound-variable hypothesis ...
frirr 5496 A well-founded relation is...
fr2nr 5497 A well-founded relation ha...
fr0 5498 Any relation is well-found...
frminex 5499 If an element of a well-fo...
efrirr 5500 A well-founded class does ...
efrn2lp 5501 A well-founded class conta...
epse 5502 The membership relation is...
tz7.2 5503 Similar to Theorem 7.2 of ...
dfepfr 5504 An alternate way of saying...
epfrc 5505 A subset of a well-founded...
wess 5506 Subset theorem for the wel...
weeq1 5507 Equality theorem for the w...
weeq2 5508 Equality theorem for the w...
wefr 5509 A well-ordering is well-fo...
weso 5510 A well-ordering is a stric...
wecmpep 5511 The elements of a class we...
wetrep 5512 On a class well-ordered by...
wefrc 5513 A nonempty subclass of a c...
we0 5514 Any relation is a well-ord...
wereu 5515 A subset of a well-ordered...
wereu2 5516 All nonempty subclasses of...
xpeq1 5533 Equality theorem for Carte...
xpss12 5534 Subset theorem for Cartesi...
xpss 5535 A Cartesian product is inc...
inxpssres 5536 Intersection with a Cartes...
relxp 5537 A Cartesian product is a r...
xpss1 5538 Subset relation for Cartes...
xpss2 5539 Subset relation for Cartes...
xpeq2 5540 Equality theorem for Carte...
elxpi 5541 Membership in a Cartesian ...
elxp 5542 Membership in a Cartesian ...
elxp2 5543 Membership in a Cartesian ...
xpeq12 5544 Equality theorem for Carte...
xpeq1i 5545 Equality inference for Car...
xpeq2i 5546 Equality inference for Car...
xpeq12i 5547 Equality inference for Car...
xpeq1d 5548 Equality deduction for Car...
xpeq2d 5549 Equality deduction for Car...
xpeq12d 5550 Equality deduction for Car...
sqxpeqd 5551 Equality deduction for a C...
nfxp 5552 Bound-variable hypothesis ...
0nelxp 5553 The empty set is not a mem...
0nelelxp 5554 A member of a Cartesian pr...
opelxp 5555 Ordered pair membership in...
opelxpi 5556 Ordered pair membership in...
opelxpd 5557 Ordered pair membership in...
opelvv 5558 Ordered pair membership in...
opelvvg 5559 Ordered pair membership in...
opelxp1 5560 The first member of an ord...
opelxp2 5561 The second member of an or...
otelxp1 5562 The first member of an ord...
otel3xp 5563 An ordered triple is an el...
opabssxpd 5564 An ordered-pair class abst...
rabxp 5565 Class abstraction restrict...
brxp 5566 Binary relation on a Carte...
pwvrel 5567 A set is a binary relation...
pwvabrel 5568 The powerclass of the cart...
brrelex12 5569 Two classes related by a b...
brrelex1 5570 If two classes are related...
brrelex2 5571 If two classes are related...
brrelex12i 5572 Two classes that are relat...
brrelex1i 5573 The first argument of a bi...
brrelex2i 5574 The second argument of a b...
nprrel12 5575 Proper classes are not rel...
nprrel 5576 No proper class is related...
0nelrel0 5577 A binary relation does not...
0nelrel 5578 A binary relation does not...
fconstmpt 5579 Representation of a consta...
vtoclr 5580 Variable to class conversi...
opthprc 5581 Justification theorem for ...
brel 5582 Two things in a binary rel...
elxp3 5583 Membership in a Cartesian ...
opeliunxp 5584 Membership in a union of C...
xpundi 5585 Distributive law for Carte...
xpundir 5586 Distributive law for Carte...
xpiundi 5587 Distributive law for Carte...
xpiundir 5588 Distributive law for Carte...
iunxpconst 5589 Membership in a union of C...
xpun 5590 The Cartesian product of t...
elvv 5591 Membership in universal cl...
elvvv 5592 Membership in universal cl...
elvvuni 5593 An ordered pair contains i...
brinxp2 5594 Intersection of binary rel...
brinxp 5595 Intersection of binary rel...
opelinxp 5596 Ordered pair element in an...
poinxp 5597 Intersection of partial or...
soinxp 5598 Intersection of total orde...
frinxp 5599 Intersection of well-found...
seinxp 5600 Intersection of set-like r...
weinxp 5601 Intersection of well-order...
posn 5602 Partial ordering of a sing...
sosn 5603 Strict ordering on a singl...
frsn 5604 Founded relation on a sing...
wesn 5605 Well-ordering of a singlet...
elopaelxp 5606 Membership in an ordered-p...
bropaex12 5607 Two classes related by an ...
opabssxp 5608 An abstraction relation is...
brab2a 5609 The law of concretion for ...
optocl 5610 Implicit substitution of c...
2optocl 5611 Implicit substitution of c...
3optocl 5612 Implicit substitution of c...
opbrop 5613 Ordered pair membership in...
0xp 5614 The Cartesian product with...
csbxp 5615 Distribute proper substitu...
releq 5616 Equality theorem for the r...
releqi 5617 Equality inference for the...
releqd 5618 Equality deduction for the...
nfrel 5619 Bound-variable hypothesis ...
sbcrel 5620 Distribute proper substitu...
relss 5621 Subclass theorem for relat...
ssrel 5622 A subclass relationship de...
eqrel 5623 Extensionality principle f...
ssrel2 5624 A subclass relationship de...
relssi 5625 Inference from subclass pr...
relssdv 5626 Deduction from subclass pr...
eqrelriv 5627 Inference from extensional...
eqrelriiv 5628 Inference from extensional...
eqbrriv 5629 Inference from extensional...
eqrelrdv 5630 Deduce equality of relatio...
eqbrrdv 5631 Deduction from extensional...
eqbrrdiv 5632 Deduction from extensional...
eqrelrdv2 5633 A version of ~ eqrelrdv . ...
ssrelrel 5634 A subclass relationship de...
eqrelrel 5635 Extensionality principle f...
elrel 5636 A member of a relation is ...
rel0 5637 The empty set is a relatio...
nrelv 5638 The universal class is not...
relsng 5639 A singleton is a relation ...
relsnb 5640 An at-most-singleton is a ...
relsnopg 5641 A singleton of an ordered ...
relsn 5642 A singleton is a relation ...
relsnop 5643 A singleton of an ordered ...
copsex2gb 5644 Implicit substitution infe...
copsex2ga 5645 Implicit substitution infe...
elopaba 5646 Membership in an ordered-p...
xpsspw 5647 A Cartesian product is inc...
unixpss 5648 The double class union of ...
relun 5649 The union of two relations...
relin1 5650 The intersection with a re...
relin2 5651 The intersection with a re...
relinxp 5652 Intersection with a Cartes...
reldif 5653 A difference cutting down ...
reliun 5654 An indexed union is a rela...
reliin 5655 An indexed intersection is...
reluni 5656 The union of a class is a ...
relint 5657 The intersection of a clas...
relopabiv 5658 A class of ordered pairs i...
relopabv 5659 A class of ordered pairs i...
relopabi 5660 A class of ordered pairs i...
relopabiALT 5661 Alternate proof of ~ relop...
relopab 5662 A class of ordered pairs i...
mptrel 5663 The maps-to notation alway...
reli 5664 The identity relation is a...
rele 5665 The membership relation is...
opabid2 5666 A relation expressed as an...
inopab 5667 Intersection of two ordere...
difopab 5668 Difference of two ordered-...
inxp 5669 Intersection of two Cartes...
xpindi 5670 Distributive law for Carte...
xpindir 5671 Distributive law for Carte...
xpiindi 5672 Distributive law for Carte...
xpriindi 5673 Distributive law for Carte...
eliunxp 5674 Membership in a union of C...
opeliunxp2 5675 Membership in a union of C...
raliunxp 5676 Write a double restricted ...
rexiunxp 5677 Write a double restricted ...
ralxp 5678 Universal quantification r...
rexxp 5679 Existential quantification...
exopxfr 5680 Transfer ordered-pair exis...
exopxfr2 5681 Transfer ordered-pair exis...
djussxp 5682 Disjoint union is a subset...
ralxpf 5683 Version of ~ ralxp with bo...
rexxpf 5684 Version of ~ rexxp with bo...
iunxpf 5685 Indexed union on a Cartesi...
opabbi2dv 5686 Deduce equality of a relat...
relop 5687 A necessary and sufficient...
ideqg 5688 For sets, the identity rel...
ideq 5689 For sets, the identity rel...
ididg 5690 A set is identical to itse...
issetid 5691 Two ways of expressing set...
coss1 5692 Subclass theorem for compo...
coss2 5693 Subclass theorem for compo...
coeq1 5694 Equality theorem for compo...
coeq2 5695 Equality theorem for compo...
coeq1i 5696 Equality inference for com...
coeq2i 5697 Equality inference for com...
coeq1d 5698 Equality deduction for com...
coeq2d 5699 Equality deduction for com...
coeq12i 5700 Equality inference for com...
coeq12d 5701 Equality deduction for com...
nfco 5702 Bound-variable hypothesis ...
brcog 5703 Ordered pair membership in...
opelco2g 5704 Ordered pair membership in...
brcogw 5705 Ordered pair membership in...
eqbrrdva 5706 Deduction from extensional...
brco 5707 Binary relation on a compo...
opelco 5708 Ordered pair membership in...
cnvss 5709 Subset theorem for convers...
cnveq 5710 Equality theorem for conve...
cnveqi 5711 Equality inference for con...
cnveqd 5712 Equality deduction for con...
elcnv 5713 Membership in a converse r...
elcnv2 5714 Membership in a converse r...
nfcnv 5715 Bound-variable hypothesis ...
brcnvg 5716 The converse of a binary r...
opelcnvg 5717 Ordered-pair membership in...
opelcnv 5718 Ordered-pair membership in...
brcnv 5719 The converse of a binary r...
csbcnv 5720 Move class substitution in...
csbcnvgALT 5721 Move class substitution in...
cnvco 5722 Distributive law of conver...
cnvuni 5723 The converse of a class un...
dfdm3 5724 Alternate definition of do...
dfrn2 5725 Alternate definition of ra...
dfrn3 5726 Alternate definition of ra...
elrn2g 5727 Membership in a range. (C...
elrng 5728 Membership in a range. (C...
elrn2 5729 Membership in a range. (C...
elrn 5730 Membership in a range. (C...
ssrelrn 5731 If a relation is a subset ...
dfdm4 5732 Alternate definition of do...
dfdmf 5733 Definition of domain, usin...
csbdm 5734 Distribute proper substitu...
eldmg 5735 Domain membership. Theore...
eldm2g 5736 Domain membership. Theore...
eldm 5737 Membership in a domain. T...
eldm2 5738 Membership in a domain. T...
dmss 5739 Subset theorem for domain....
dmeq 5740 Equality theorem for domai...
dmeqi 5741 Equality inference for dom...
dmeqd 5742 Equality deduction for dom...
opeldmd 5743 Membership of first of an ...
opeldm 5744 Membership of first of an ...
breldm 5745 Membership of first of a b...
breldmg 5746 Membership of first of a b...
dmun 5747 The domain of a union is t...
dmin 5748 The domain of an intersect...
breldmd 5749 Membership of first of a b...
dmiun 5750 The domain of an indexed u...
dmuni 5751 The domain of a union. Pa...
dmopab 5752 The domain of a class of o...
dmopabelb 5753 A set is an element of the...
dmopab2rex 5754 The domain of an ordered p...
dmopabss 5755 Upper bound for the domain...
dmopab3 5756 The domain of a restricted...
dm0 5757 The domain of the empty se...
dmi 5758 The domain of the identity...
dmv 5759 The domain of the universe...
dmep 5760 The domain of the membersh...
domepOLD 5761 Obsolete proof of ~ dmep a...
dm0rn0 5762 An empty domain is equival...
rn0 5763 The range of the empty set...
rnep 5764 The range of the membershi...
reldm0 5765 A relation is empty iff it...
dmxp 5766 The domain of a Cartesian ...
dmxpid 5767 The domain of a Cartesian ...
dmxpin 5768 The domain of the intersec...
xpid11 5769 The Cartesian square is a ...
dmcnvcnv 5770 The domain of the double c...
rncnvcnv 5771 The range of the double co...
elreldm 5772 The first member of an ord...
rneq 5773 Equality theorem for range...
rneqi 5774 Equality inference for ran...
rneqd 5775 Equality deduction for ran...
rnss 5776 Subset theorem for range. ...
rnssi 5777 Subclass inference for ran...
brelrng 5778 The second argument of a b...
brelrn 5779 The second argument of a b...
opelrn 5780 Membership of second membe...
releldm 5781 The first argument of a bi...
relelrn 5782 The second argument of a b...
releldmb 5783 Membership in a domain. (...
relelrnb 5784 Membership in a range. (C...
releldmi 5785 The first argument of a bi...
relelrni 5786 The second argument of a b...
dfrnf 5787 Definition of range, using...
nfdm 5788 Bound-variable hypothesis ...
nfrn 5789 Bound-variable hypothesis ...
dmiin 5790 Domain of an intersection....
rnopab 5791 The range of a class of or...
rnmpt 5792 The range of a function in...
elrnmpt 5793 The range of a function in...
elrnmpt1s 5794 Elementhood in an image se...
elrnmpt1 5795 Elementhood in an image se...
elrnmptg 5796 Membership in the range of...
elrnmpti 5797 Membership in the range of...
elrnmptd 5798 The range of a function in...
elrnmptdv 5799 Elementhood in the range o...
elrnmpt2d 5800 Elementhood in the range o...
dfiun3g 5801 Alternate definition of in...
dfiin3g 5802 Alternate definition of in...
dfiun3 5803 Alternate definition of in...
dfiin3 5804 Alternate definition of in...
riinint 5805 Express a relative indexed...
relrn0 5806 A relation is empty iff it...
dmrnssfld 5807 The domain and range of a ...
dmcoss 5808 Domain of a composition. ...
rncoss 5809 Range of a composition. (...
dmcosseq 5810 Domain of a composition. ...
dmcoeq 5811 Domain of a composition. ...
rncoeq 5812 Range of a composition. (...
reseq1 5813 Equality theorem for restr...
reseq2 5814 Equality theorem for restr...
reseq1i 5815 Equality inference for res...
reseq2i 5816 Equality inference for res...
reseq12i 5817 Equality inference for res...
reseq1d 5818 Equality deduction for res...
reseq2d 5819 Equality deduction for res...
reseq12d 5820 Equality deduction for res...
nfres 5821 Bound-variable hypothesis ...
csbres 5822 Distribute proper substitu...
res0 5823 A restriction to the empty...
dfres3 5824 Alternate definition of re...
opelres 5825 Ordered pair elementhood i...
brres 5826 Binary relation on a restr...
opelresi 5827 Ordered pair membership in...
brresi 5828 Binary relation on a restr...
opres 5829 Ordered pair membership in...
resieq 5830 A restricted identity rela...
opelidres 5831 ` <. A , A >. ` belongs to...
resres 5832 The restriction of a restr...
resundi 5833 Distributive law for restr...
resundir 5834 Distributive law for restr...
resindi 5835 Class restriction distribu...
resindir 5836 Class restriction distribu...
inres 5837 Move intersection into cla...
resdifcom 5838 Commutative law for restri...
resiun1 5839 Distribution of restrictio...
resiun2 5840 Distribution of restrictio...
dmres 5841 The domain of a restrictio...
ssdmres 5842 A domain restricted to a s...
dmresexg 5843 The domain of a restrictio...
resss 5844 A class includes its restr...
rescom 5845 Commutative law for restri...
ssres 5846 Subclass theorem for restr...
ssres2 5847 Subclass theorem for restr...
relres 5848 A restriction is a relatio...
resabs1 5849 Absorption law for restric...
resabs1d 5850 Absorption law for restric...
resabs2 5851 Absorption law for restric...
residm 5852 Idempotent law for restric...
resima 5853 A restriction to an image....
resima2 5854 Image under a restricted c...
rnresss 5855 The range of a restriction...
xpssres 5856 Restriction of a constant ...
elinxp 5857 Membership in an intersect...
elres 5858 Membership in a restrictio...
elsnres 5859 Membership in restriction ...
relssres 5860 Simplification law for res...
dmressnsn 5861 The domain of a restrictio...
eldmressnsn 5862 The element of the domain ...
eldmeldmressn 5863 An element of the domain (...
resdm 5864 A relation restricted to i...
resexg 5865 The restriction of a set i...
resexd 5866 The restriction of a set i...
resex 5867 The restriction of a set i...
resindm 5868 When restricting a relatio...
resdmdfsn 5869 Restricting a relation to ...
resopab 5870 Restriction of a class abs...
iss 5871 A subclass of the identity...
resopab2 5872 Restriction of a class abs...
resmpt 5873 Restriction of the mapping...
resmpt3 5874 Unconditional restriction ...
resmptf 5875 Restriction of the mapping...
resmptd 5876 Restriction of the mapping...
dfres2 5877 Alternate definition of th...
mptss 5878 Sufficient condition for i...
elidinxp 5879 Characterization of the el...
elidinxpid 5880 Characterization of the el...
elrid 5881 Characterization of the el...
idinxpres 5882 The intersection of the id...
idinxpresid 5883 The intersection of the id...
idssxp 5884 A diagonal set as a subset...
opabresid 5885 The restricted identity re...
mptresid 5886 The restricted identity re...
opabresidOLD 5887 Obsolete version of ~ opab...
mptresidOLD 5888 Obsolete version of ~ mptr...
dmresi 5889 The domain of a restricted...
restidsing 5890 Restriction of the identit...
iresn0n0 5891 The identity function rest...
imaeq1 5892 Equality theorem for image...
imaeq2 5893 Equality theorem for image...
imaeq1i 5894 Equality theorem for image...
imaeq2i 5895 Equality theorem for image...
imaeq1d 5896 Equality theorem for image...
imaeq2d 5897 Equality theorem for image...
imaeq12d 5898 Equality theorem for image...
dfima2 5899 Alternate definition of im...
dfima3 5900 Alternate definition of im...
elimag 5901 Membership in an image. T...
elima 5902 Membership in an image. T...
elima2 5903 Membership in an image. T...
elima3 5904 Membership in an image. T...
nfima 5905 Bound-variable hypothesis ...
nfimad 5906 Deduction version of bound...
imadmrn 5907 The image of the domain of...
imassrn 5908 The image of a class is a ...
mptima 5909 Image of a function in map...
imai 5910 Image under the identity r...
rnresi 5911 The range of the restricte...
resiima 5912 The image of a restriction...
ima0 5913 Image of the empty set. T...
0ima 5914 Image under the empty rela...
csbima12 5915 Move class substitution in...
imadisj 5916 A class whose image under ...
cnvimass 5917 A preimage under any class...
cnvimarndm 5918 The preimage of the range ...
imasng 5919 The image of a singleton. ...
relimasn 5920 The image of a singleton. ...
elrelimasn 5921 Elementhood in the image o...
elimasn 5922 Membership in an image of ...
elimasng 5923 Membership in an image of ...
elimasni 5924 Membership in an image of ...
args 5925 Two ways to express the cl...
eliniseg 5926 Membership in an initial s...
epini 5927 Any set is equal to its pr...
iniseg 5928 An idiom that signifies an...
inisegn0 5929 Nonemptiness of an initial...
dffr3 5930 Alternate definition of we...
dfse2 5931 Alternate definition of se...
imass1 5932 Subset theorem for image. ...
imass2 5933 Subset theorem for image. ...
ndmima 5934 The image of a singleton o...
relcnv 5935 A converse is a relation. ...
relbrcnvg 5936 When ` R ` is a relation, ...
eliniseg2 5937 Eliminate the class existe...
relbrcnv 5938 When ` R ` is a relation, ...
cotrg 5939 Two ways of saying that th...
cotr 5940 Two ways of saying a relat...
idrefALT 5941 Alternate proof of ~ idref...
cnvsym 5942 Two ways of saying a relat...
intasym 5943 Two ways of saying a relat...
asymref 5944 Two ways of saying a relat...
asymref2 5945 Two ways of saying a relat...
intirr 5946 Two ways of saying a relat...
brcodir 5947 Two ways of saying that tw...
codir 5948 Two ways of saying a relat...
qfto 5949 A quantifier-free way of e...
xpidtr 5950 A Cartesian square is a tr...
trin2 5951 The intersection of two tr...
poirr2 5952 A partial order relation i...
trinxp 5953 The relation induced by a ...
soirri 5954 A strict order relation is...
sotri 5955 A strict order relation is...
son2lpi 5956 A strict order relation ha...
sotri2 5957 A transitivity relation. ...
sotri3 5958 A transitivity relation. ...
poleloe 5959 Express "less than or equa...
poltletr 5960 Transitive law for general...
somin1 5961 Property of a minimum in a...
somincom 5962 Commutativity of minimum i...
somin2 5963 Property of a minimum in a...
soltmin 5964 Being less than a minimum,...
cnvopab 5965 The converse of a class ab...
mptcnv 5966 The converse of a mapping ...
cnv0 5967 The converse of the empty ...
cnvi 5968 The converse of the identi...
cnvun 5969 The converse of a union is...
cnvdif 5970 Distributive law for conve...
cnvin 5971 Distributive law for conve...
rnun 5972 Distributive law for range...
rnin 5973 The range of an intersecti...
rniun 5974 The range of an indexed un...
rnuni 5975 The range of a union. Par...
imaundi 5976 Distributive law for image...
imaundir 5977 The image of a union. (Co...
cnvimassrndm 5978 The preimage of a superset...
dminss 5979 An upper bound for interse...
imainss 5980 An upper bound for interse...
inimass 5981 The image of an intersecti...
inimasn 5982 The intersection of the im...
cnvxp 5983 The converse of a Cartesia...
xp0 5984 The Cartesian product with...
xpnz 5985 The Cartesian product of n...
xpeq0 5986 At least one member of an ...
xpdisj1 5987 Cartesian products with di...
xpdisj2 5988 Cartesian products with di...
xpsndisj 5989 Cartesian products with tw...
difxp 5990 Difference of Cartesian pr...
difxp1 5991 Difference law for Cartesi...
difxp2 5992 Difference law for Cartesi...
djudisj 5993 Disjoint unions with disjo...
xpdifid 5994 The set of distinct couple...
resdisj 5995 A double restriction to di...
rnxp 5996 The range of a Cartesian p...
dmxpss 5997 The domain of a Cartesian ...
rnxpss 5998 The range of a Cartesian p...
rnxpid 5999 The range of a Cartesian s...
ssxpb 6000 A Cartesian product subcla...
xp11 6001 The Cartesian product of n...
xpcan 6002 Cancellation law for Carte...
xpcan2 6003 Cancellation law for Carte...
ssrnres 6004 Two ways to express surjec...
rninxp 6005 Two ways to express surjec...
dminxp 6006 Two ways to express totali...
imainrect 6007 Image by a restricted and ...
xpima 6008 Direct image by a Cartesia...
xpima1 6009 Direct image by a Cartesia...
xpima2 6010 Direct image by a Cartesia...
xpimasn 6011 Direct image of a singleto...
sossfld 6012 The base set of a strict o...
sofld 6013 The base set of a nonempty...
cnvcnv3 6014 The set of all ordered pai...
dfrel2 6015 Alternate definition of re...
dfrel4v 6016 A relation can be expresse...
dfrel4 6017 A relation can be expresse...
cnvcnv 6018 The double converse of a c...
cnvcnv2 6019 The double converse of a c...
cnvcnvss 6020 The double converse of a c...
cnvrescnv 6021 Two ways to express the co...
cnveqb 6022 Equality theorem for conve...
cnveq0 6023 A relation empty iff its c...
dfrel3 6024 Alternate definition of re...
elid 6025 Characterization of the el...
dmresv 6026 The domain of a universal ...
rnresv 6027 The range of a universal r...
dfrn4 6028 Range defined in terms of ...
csbrn 6029 Distribute proper substitu...
rescnvcnv 6030 The restriction of the dou...
cnvcnvres 6031 The double converse of the...
imacnvcnv 6032 The image of the double co...
dmsnn0 6033 The domain of a singleton ...
rnsnn0 6034 The range of a singleton i...
dmsn0 6035 The domain of the singleto...
cnvsn0 6036 The converse of the single...
dmsn0el 6037 The domain of a singleton ...
relsn2 6038 A singleton is a relation ...
dmsnopg 6039 The domain of a singleton ...
dmsnopss 6040 The domain of a singleton ...
dmpropg 6041 The domain of an unordered...
dmsnop 6042 The domain of a singleton ...
dmprop 6043 The domain of an unordered...
dmtpop 6044 The domain of an unordered...
cnvcnvsn 6045 Double converse of a singl...
dmsnsnsn 6046 The domain of the singleto...
rnsnopg 6047 The range of a singleton o...
rnpropg 6048 The range of a pair of ord...
cnvsng 6049 Converse of a singleton of...
rnsnop 6050 The range of a singleton o...
op1sta 6051 Extract the first member o...
cnvsn 6052 Converse of a singleton of...
op2ndb 6053 Extract the second member ...
op2nda 6054 Extract the second member ...
opswap 6055 Swap the members of an ord...
cnvresima 6056 An image under the convers...
resdm2 6057 A class restricted to its ...
resdmres 6058 Restriction to the domain ...
resresdm 6059 A restriction by an arbitr...
imadmres 6060 The image of the domain of...
resdmss 6061 Subset relationship for th...
resdifdi 6062 Distributive law for restr...
resdifdir 6063 Distributive law for restr...
mptpreima 6064 The preimage of a function...
mptiniseg 6065 Converse singleton image o...
dmmpt 6066 The domain of the mapping ...
dmmptss 6067 The domain of a mapping is...
dmmptg 6068 The domain of the mapping ...
rnmpt0f 6069 The range of a function in...
rnmptn0 6070 The range of a function in...
relco 6071 A composition is a relatio...
dfco2 6072 Alternate definition of a ...
dfco2a 6073 Generalization of ~ dfco2 ...
coundi 6074 Class composition distribu...
coundir 6075 Class composition distribu...
cores 6076 Restricted first member of...
resco 6077 Associative law for the re...
imaco 6078 Image of the composition o...
rnco 6079 The range of the compositi...
rnco2 6080 The range of the compositi...
dmco 6081 The domain of a compositio...
coeq0 6082 A composition of two relat...
coiun 6083 Composition with an indexe...
cocnvcnv1 6084 A composition is not affec...
cocnvcnv2 6085 A composition is not affec...
cores2 6086 Absorption of a reverse (p...
co02 6087 Composition with the empty...
co01 6088 Composition with the empty...
coi1 6089 Composition with the ident...
coi2 6090 Composition with the ident...
coires1 6091 Composition with a restric...
coass 6092 Associative law for class ...
relcnvtrg 6093 General form of ~ relcnvtr...
relcnvtr 6094 A relation is transitive i...
relssdmrn 6095 A relation is included in ...
resssxp 6096 If the ` R ` -image of a c...
cnvssrndm 6097 The converse is a subset o...
cossxp 6098 Composition as a subset of...
relrelss 6099 Two ways to describe the s...
unielrel 6100 The membership relation fo...
relfld 6101 The double union of a rela...
relresfld 6102 Restriction of a relation ...
relcoi2 6103 Composition with the ident...
relcoi1 6104 Composition with the ident...
unidmrn 6105 The double union of the co...
relcnvfld 6106 if ` R ` is a relation, it...
dfdm2 6107 Alternate definition of do...
unixp 6108 The double class union of ...
unixp0 6109 A Cartesian product is emp...
unixpid 6110 Field of a Cartesian squar...
ressn 6111 Restriction of a class to ...
cnviin 6112 The converse of an interse...
cnvpo 6113 The converse of a partial ...
cnvso 6114 The converse of a strict o...
xpco 6115 Composition of two Cartesi...
xpcoid 6116 Composition of two Cartesi...
elsnxp 6117 Membership in a Cartesian ...
reu3op 6118 There is a unique ordered ...
reuop 6119 There is a unique ordered ...
opreu2reurex 6120 There is a unique ordered ...
opreu2reu 6121 If there is a unique order...
predeq123 6124 Equality theorem for the p...
predeq1 6125 Equality theorem for the p...
predeq2 6126 Equality theorem for the p...
predeq3 6127 Equality theorem for the p...
nfpred 6128 Bound-variable hypothesis ...
predpredss 6129 If ` A ` is a subset of ` ...
predss 6130 The predecessor class of `...
sspred 6131 Another subset/predecessor...
dfpred2 6132 An alternate definition of...
dfpred3 6133 An alternate definition of...
dfpred3g 6134 An alternate definition of...
elpredim 6135 Membership in a predecesso...
elpred 6136 Membership in a predecesso...
elpredg 6137 Membership in a predecesso...
predasetex 6138 The predecessor class exis...
dffr4 6139 Alternate definition of we...
predel 6140 Membership in the predeces...
predpo 6141 Property of the precessor ...
predso 6142 Property of the predecesso...
predbrg 6143 Closed form of ~ elpredim ...
setlikespec 6144 If ` R ` is set-like in ` ...
predidm 6145 Idempotent law for the pre...
predin 6146 Intersection law for prede...
predun 6147 Union law for predecessor ...
preddif 6148 Difference law for predece...
predep 6149 The predecessor under the ...
preddowncl 6150 A property of classes that...
predpoirr 6151 Given a partial ordering, ...
predfrirr 6152 Given a well-founded relat...
pred0 6153 The predecessor class over...
tz6.26 6154 All nonempty subclasses of...
tz6.26i 6155 All nonempty subclasses of...
wfi 6156 The Principle of Well-Foun...
wfii 6157 The Principle of Well-Foun...
wfisg 6158 Well-Founded Induction Sch...
wfis 6159 Well-Founded Induction Sch...
wfis2fg 6160 Well-Founded Induction Sch...
wfis2f 6161 Well Founded Induction sch...
wfis2g 6162 Well-Founded Induction Sch...
wfis2 6163 Well Founded Induction sch...
wfis3 6164 Well Founded Induction sch...
ordeq 6173 Equality theorem for the o...
elong 6174 An ordinal number is an or...
elon 6175 An ordinal number is an or...
eloni 6176 An ordinal number has the ...
elon2 6177 An ordinal number is an or...
limeq 6178 Equality theorem for the l...
ordwe 6179 Membership well-orders eve...
ordtr 6180 An ordinal class is transi...
ordfr 6181 Membership is well-founded...
ordelss 6182 An element of an ordinal c...
trssord 6183 A transitive subclass of a...
ordirr 6184 No ordinal class is a memb...
nordeq 6185 A member of an ordinal cla...
ordn2lp 6186 An ordinal class cannot be...
tz7.5 6187 A nonempty subclass of an ...
ordelord 6188 An element of an ordinal c...
tron 6189 The class of all ordinal n...
ordelon 6190 An element of an ordinal c...
onelon 6191 An element of an ordinal n...
tz7.7 6192 A transitive class belongs...
ordelssne 6193 For ordinal classes, membe...
ordelpss 6194 For ordinal classes, membe...
ordsseleq 6195 For ordinal classes, inclu...
ordin 6196 The intersection of two or...
onin 6197 The intersection of two or...
ordtri3or 6198 A trichotomy law for ordin...
ordtri1 6199 A trichotomy law for ordin...
ontri1 6200 A trichotomy law for ordin...
ordtri2 6201 A trichotomy law for ordin...
ordtri3 6202 A trichotomy law for ordin...
ordtri4 6203 A trichotomy law for ordin...
orddisj 6204 An ordinal class and its s...
onfr 6205 The ordinal class is well-...
onelpss