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

List of Theorems
RefDescription
dummylink 1 (_Note_: This inference r...
idi 2 Inference form of ~ id . ...
mp2 9 A double modus ponens infe...
mp2b 10 A double modus ponens infe...
a1i 11 Inference derived from axi...
mp1i 12 Drop and replace an antece...
a2i 13 Inference derived from axi...
imim2i 14 Inference adding common an...
mpd 15 A modus ponens deduction. ...
syl 16 An inference version of th...
mpi 17 A nested modus ponens infe...
mp2ALT 18 Alternate proof of ~ mp2 (...
3syl 19 Inference chaining two syl...
id 20 Principle of identity. Th...
id1 21 Principle of identity. Th...
idd 22 Principle of identity with...
a1d 23 Deduction introducing an e...
a2d 24 Deduction distributing an ...
a1ii 25 Add two antecedents to a w...
a1iiALT 26 Alternate proof of ~ a1ii ...
sylcom 27 Syllogism inference with c...
syl5com 28 Syllogism inference with c...
com12 29 Inference that swaps (comm...
syl5 30 A syllogism rule of infere...
syl6 31 A syllogism rule of infere...
syl56 32 Combine ~ syl5 and ~ syl6 ...
syl6com 33 Syllogism inference with c...
mpcom 34 Modus ponens inference wit...
syli 35 Syllogism inference with c...
syl2im 36 Replace two antecedents. ...
pm2.27 37 This theorem, called "Asse...
mpdd 38 A nested modus ponens dedu...
mpid 39 A nested modus ponens dedu...
mpdi 40 A nested modus ponens dedu...
mpii 41 A doubly nested modus pone...
syld 42 Syllogism deduction. (Con...
mp2d 43 A double modus ponens dedu...
a1dd 44 Deduction introducing a ne...
pm2.43i 45 Inference absorbing redund...
pm2.43d 46 Deduction absorbing redund...
pm2.43a 47 Inference absorbing redund...
pm2.43b 48 Inference absorbing redund...
pm2.43 49 Absorption of redundant an...
imim2d 50 Deduction adding nested an...
imim2 51 A closed form of syllogism...
embantd 52 Deduction embedding an ant...
3syld 53 Triple syllogism deduction...
sylsyld 54 Virtual deduction rule ~ e...
imim12i 55 Inference joining two impl...
imim1i 56 Inference adding common co...
imim3i 57 Inference adding three nes...
sylc 58 A syllogism inference comb...
syl3c 59 A syllogism inference comb...
syl6mpi 60 ~ e20 without virtual dedu...
mpsyl 61 Modus ponens combined with...
syl6c 62 Inference combining ~ syl6...
syldd 63 Nested syllogism deduction...
syl5d 64 A nested syllogism deducti...
syl7 65 A syllogism rule of infere...
syl6d 66 A nested syllogism deducti...
syl8 67 A syllogism rule of infere...
syl9 68 A nested syllogism inferen...
syl9r 69 A nested syllogism inferen...
imim12d 70 Deduction combining antece...
imim1d 71 Deduction adding nested co...
imim1 72 A closed form of syllogism...
pm2.83 73 Theorem *2.83 of [Whitehea...
com23 74 Commutation of antecedents...
com3r 75 Commutation of antecedents...
com13 76 Commutation of antecedents...
com3l 77 Commutation of antecedents...
pm2.04 78 Swap antecedents. Theorem...
com34 79 Commutation of antecedents...
com4l 80 Commutation of antecedents...
com4t 81 Commutation of antecedents...
com4r 82 Commutation of antecedents...
com24 83 Commutation of antecedents...
com14 84 Commutation of antecedents...
com45 85 Commutation of antecedents...
com35 86 Commutation of antecedents...
com25 87 Commutation of antecedents...
com5l 88 Commutation of antecedents...
com15 89 Commutation of antecedents...
com52l 90 Commutation of antecedents...
com52r 91 Commutation of antecedents...
com5r 92 Commutation of antecedents...
jarr 93 Elimination of a nested an...
pm2.86i 94 Inference based on ~ pm2.8...
pm2.86d 95 Deduction based on ~ pm2.8...
pm2.86 96 Converse of axiom ~ ax-2 ....
loolin 97 The Linearity Axiom of the...
loowoz 98 An alternate for the Linea...
con4d 99 Deduction derived from axi...
pm2.21d 100 A contradiction implies an...
pm2.21dd 101 A contradiction implies an...
pm2.21 102 From a wff and its negatio...
pm2.24 103 Theorem *2.24 of [Whitehea...
pm2.18 104 Proof by contradiction. T...
pm2.18d 105 Deduction based on reducti...
notnot2 106 Converse of double negatio...
notnotrd 107 Deduction converting doubl...
notnotri 108 Inference from double nega...
con2d 109 A contraposition deduction...
con2 110 Contraposition. Theorem *...
mt2d 111 Modus tollens deduction. ...
mt2i 112 Modus tollens inference. ...
nsyl3 113 A negated syllogism infere...
con2i 114 A contraposition inference...
nsyl 115 A negated syllogism infere...
notnot1 116 Converse of double negatio...
notnoti 117 Infer double negation. (C...
con1d 118 A contraposition deduction...
mt3d 119 Modus tollens deduction. ...
mt3i 120 Modus tollens inference. ...
nsyl2 121 A negated syllogism infere...
con1 122 Contraposition. Theorem *...
con1i 123 A contraposition inference...
con4i 124 Inference rule derived fro...
pm2.21i 125 A contradiction implies an...
pm2.24ii 126 A contradiction implies an...
con3d 127 A contraposition deduction...
con3 128 Contraposition. Theorem *...
con3i 129 A contraposition inference...
con3rr3 130 Rotate through consequent ...
mt4 131 The rule of modus tollens....
mt4d 132 Modus tollens deduction. ...
mt4i 133 Modus tollens inference. ...
nsyld 134 A negated syllogism deduct...
nsyli 135 A negated syllogism infere...
nsyl4 136 A negated syllogism infere...
pm2.24d 137 Deduction version of ~ pm2...
pm2.24i 138 Inference version of ~ pm2...
pm3.2im 139 Theorem *3.2 of [Whitehead...
mth8 140 Theorem 8 of [Margaris] p....
jc 141 Inference joining the cons...
impi 142 An importation inference. ...
expi 143 An exportation inference. ...
simprim 144 Simplification. Similar t...
simplim 145 Simplification. Similar t...
pm2.5 146 Theorem *2.5 of [Whitehead...
pm2.51 147 Theorem *2.51 of [Whitehea...
pm2.521 148 Theorem *2.521 of [Whitehe...
pm2.52 149 Theorem *2.52 of [Whitehea...
expt 150 Exportation theorem expres...
impt 151 Importation theorem expres...
pm2.61d 152 Deduction eliminating an a...
pm2.61d1 153 Inference eliminating an a...
pm2.61d2 154 Inference eliminating an a...
ja 155 Inference joining the ante...
jad 156 Deduction form of ~ ja . ...
jarl 157 Elimination of a nested an...
pm2.61i 158 Inference eliminating an a...
pm2.61ii 159 Inference eliminating two ...
pm2.61nii 160 Inference eliminating two ...
pm2.61iii 161 Inference eliminating thre...
pm2.01 162 Reductio ad absurdum. The...
pm2.01d 163 Deduction based on reducti...
pm2.6 164 Theorem *2.6 of [Whitehead...
pm2.61 165 Theorem *2.61 of [Whitehea...
pm2.65 166 Theorem *2.65 of [Whitehea...
pm2.65i 167 Inference rule for proof b...
pm2.65d 168 Deduction rule for proof b...
mto 169 The rule of modus tollens....
mtod 170 Modus tollens deduction. ...
mtoi 171 Modus tollens inference. ...
mt2 172 A rule similar to modus to...
mt3 173 A rule similar to modus to...
peirce 174 Peirce's axiom. This odd-...
looinv 175 The Inversion Axiom of the...
bijust 176 Theorem used to justify de...
bi1 179 Property of the biconditio...
bi3 180 Property of the biconditio...
impbii 181 Infer an equivalence from ...
impbidd 182 Deduce an equivalence from...
impbid21d 183 Deduce an equivalence from...
impbid 184 Deduce an equivalence from...
dfbi1 185 Relate the biconditional c...
dfbi1gb 186 This proof of ~ dfbi1 , di...
biimpi 187 Infer an implication from ...
sylbi 188 A mixed syllogism inferenc...
sylib 189 A mixed syllogism inferenc...
bi2 190 Property of the biconditio...
bicom1 191 Commutative law for equiva...
bicom 192 Commutative law for equiva...
bicomd 193 Commute two sides of a bic...
bicomi 194 Inference from commutative...
impbid1 195 Infer an equivalence from ...
impbid2 196 Infer an equivalence from ...
impcon4bid 197 A variation on ~ impbid wi...
biimpri 198 Infer a converse implicati...
biimpd 199 Deduce an implication from...
mpbi 200 An inference from a bicond...
mpbir 201 An inference from a bicond...
mpbid 202 A deduction from a bicondi...
mpbii 203 An inference from a nested...
sylibr 204 A mixed syllogism inferenc...
sylbir 205 A mixed syllogism inferenc...
sylibd 206 A syllogism deduction. (C...
sylbid 207 A syllogism deduction. (C...
mpbidi 208 A deduction from a bicondi...
syl5bi 209 A mixed syllogism inferenc...
syl5bir 210 A mixed syllogism inferenc...
syl5ib 211 A mixed syllogism inferenc...
syl5ibcom 212 A mixed syllogism inferenc...
syl5ibr 213 A mixed syllogism inferenc...
syl5ibrcom 214 A mixed syllogism inferenc...
biimprd 215 Deduce a converse implicat...
biimpcd 216 Deduce a commuted implicat...
biimprcd 217 Deduce a converse commuted...
syl6ib 218 A mixed syllogism inferenc...
syl6ibr 219 A mixed syllogism inferenc...
syl6bi 220 A mixed syllogism inferenc...
syl6bir 221 A mixed syllogism inferenc...
syl7bi 222 A mixed syllogism inferenc...
syl8ib 223 A syllogism rule of infere...
mpbird 224 A deduction from a bicondi...
mpbiri 225 An inference from a nested...
sylibrd 226 A syllogism deduction. (C...
sylbird 227 A syllogism deduction. (C...
biid 228 Principle of identity for ...
biidd 229 Principle of identity with...
pm5.1im 230 Two propositions are equiv...
2th 231 Two truths are equivalent....
2thd 232 Two truths are equivalent ...
ibi 233 Inference that converts a ...
ibir 234 Inference that converts a ...
ibd 235 Deduction that converts a ...
pm5.74 236 Distribution of implicatio...
pm5.74i 237 Distribution of implicatio...
pm5.74ri 238 Distribution of implicatio...
pm5.74d 239 Distribution of implicatio...
pm5.74rd 240 Distribution of implicatio...
bitri 241 An inference from transiti...
bitr2i 242 An inference from transiti...
bitr3i 243 An inference from transiti...
bitr4i 244 An inference from transiti...
bitrd 245 Deduction form of ~ bitri ...
bitr2d 246 Deduction form of ~ bitr2i...
bitr3d 247 Deduction form of ~ bitr3i...
bitr4d 248 Deduction form of ~ bitr4i...
syl5bb 249 A syllogism inference from...
syl5rbb 250 A syllogism inference from...
syl5bbr 251 A syllogism inference from...
syl5rbbr 252 A syllogism inference from...
syl6bb 253 A syllogism inference from...
syl6rbb 254 A syllogism inference from...
syl6bbr 255 A syllogism inference from...
syl6rbbr 256 A syllogism inference from...
3imtr3i 257 A mixed syllogism inferenc...
3imtr4i 258 A mixed syllogism inferenc...
3imtr3d 259 More general version of ~ ...
3imtr4d 260 More general version of ~ ...
3imtr3g 261 More general version of ~ ...
3imtr4g 262 More general version of ~ ...
3bitri 263 A chained inference from t...
3bitrri 264 A chained inference from t...
3bitr2i 265 A chained inference from t...
3bitr2ri 266 A chained inference from t...
3bitr3i 267 A chained inference from t...
3bitr3ri 268 A chained inference from t...
3bitr4i 269 A chained inference from t...
3bitr4ri 270 A chained inference from t...
3bitrd 271 Deduction from transitivit...
3bitrrd 272 Deduction from transitivit...
3bitr2d 273 Deduction from transitivit...
3bitr2rd 274 Deduction from transitivit...
3bitr3d 275 Deduction from transitivit...
3bitr3rd 276 Deduction from transitivit...
3bitr4d 277 Deduction from transitivit...
3bitr4rd 278 Deduction from transitivit...
3bitr3g 279 More general version of ~ ...
3bitr4g 280 More general version of ~ ...
bi3ant 281 Construct a bi-conditional...
bisym 282 Express symmetries of theo...
notnot 283 Double negation. Theorem ...
con34b 284 Contraposition. Theorem *...
con4bid 285 A contraposition deduction...
notbid 286 Deduction negating both si...
notbi 287 Contraposition. Theorem *...
notbii 288 Negate both sides of a log...
con4bii 289 A contraposition inference...
mtbi 290 An inference from a bicond...
mtbir 291 An inference from a bicond...
mtbid 292 A deduction from a bicondi...
mtbird 293 A deduction from a bicondi...
mtbii 294 An inference from a bicond...
mtbiri 295 An inference from a bicond...
sylnib 296 A mixed syllogism inferenc...
sylnibr 297 A mixed syllogism inferenc...
sylnbi 298 A mixed syllogism inferenc...
sylnbir 299 A mixed syllogism inferenc...
xchnxbi 300 Replacement of a subexpres...
xchnxbir 301 Replacement of a subexpres...
xchbinx 302 Replacement of a subexpres...
xchbinxr 303 Replacement of a subexpres...
imbi2i 304 Introduce an antecedent to...
bibi2i 305 Inference adding a bicondi...
bibi1i 306 Inference adding a bicondi...
bibi12i 307 The equivalence of two equ...
imbi2d 308 Deduction adding an antece...
imbi1d 309 Deduction adding a consequ...
bibi2d 310 Deduction adding a bicondi...
bibi1d 311 Deduction adding a bicondi...
imbi12d 312 Deduction joining two equi...
bibi12d 313 Deduction joining two equi...
imbi1 314 Theorem *4.84 of [Whitehea...
imbi2 315 Theorem *4.85 of [Whitehea...
imbi1i 316 Introduce a consequent to ...
imbi12i 317 Join two logical equivalen...
bibi1 318 Theorem *4.86 of [Whitehea...
con2bi 319 Contraposition. Theorem *...
con2bid 320 A contraposition deduction...
con1bid 321 A contraposition deduction...
con1bii 322 A contraposition inference...
con2bii 323 A contraposition inference...
con1b 324 Contraposition. Bidirecti...
con2b 325 Contraposition. Bidirecti...
biimt 326 A wff is equivalent to its...
pm5.5 327 Theorem *5.5 of [Whitehead...
a1bi 328 Inference rule introducing...
mt2bi 329 A false consequent falsifi...
mtt 330 Modus-tollens-like theorem...
pm5.501 331 Theorem *5.501 of [Whitehe...
ibib 332 Implication in terms of im...
ibibr 333 Implication in terms of im...
tbt 334 A wff is equivalent to its...
nbn2 335 The negation of a wff is e...
bibif 336 Transfer negation via an e...
nbn 337 The negation of a wff is e...
nbn3 338 Transfer falsehood via equ...
pm5.21im 339 Two propositions are equiv...
2false 340 Two falsehoods are equival...
2falsed 341 Two falsehoods are equival...
pm5.21ni 342 Two propositions implying ...
pm5.21nii 343 Eliminate an antecedent im...
pm5.21ndd 344 Eliminate an antecedent im...
bija 345 Combine antecedents into a...
pm5.18 346 Theorem *5.18 of [Whitehea...
xor3 347 Two ways to express "exclu...
nbbn 348 Move negation outside of b...
biass 349 Associative law for the bi...
pm5.19 350 Theorem *5.19 of [Whitehea...
bi2.04 351 Logical equivalence of com...
pm5.4 352 Antecedent absorption impl...
imdi 353 Distributive law for impli...
pm5.41 354 Theorem *5.41 of [Whitehea...
pm4.8 355 Theorem *4.8 of [Whitehead...
pm4.81 356 Theorem *4.81 of [Whitehea...
imim21b 357 Simplify an implication be...
pm4.64 362 Theorem *4.64 of [Whitehea...
pm2.53 363 Theorem *2.53 of [Whitehea...
pm2.54 364 Theorem *2.54 of [Whitehea...
ori 365 Infer implication from dis...
orri 366 Infer implication from dis...
ord 367 Deduce implication from di...
orrd 368 Deduce implication from di...
jaoi 369 Inference disjoining the a...
jaod 370 Deduction disjoining the a...
mpjaod 371 Eliminate a disjunction in...
orel1 372 Elimination of disjunction...
orel2 373 Elimination of disjunction...
olc 374 Introduction of a disjunct...
orc 375 Introduction of a disjunct...
pm1.4 376 Axiom *1.4 of [WhiteheadRu...
orcom 377 Commutative law for disjun...
orcomd 378 Commutation of disjuncts i...
orcoms 379 Commutation of disjuncts i...
orci 380 Deduction introducing a di...
olci 381 Deduction introducing a di...
orcd 382 Deduction introducing a di...
olcd 383 Deduction introducing a di...
orcs 384 Deduction eliminating disj...
olcs 385 Deduction eliminating disj...
pm2.07 386 Theorem *2.07 of [Whitehea...
pm2.45 387 Theorem *2.45 of [Whitehea...
pm2.46 388 Theorem *2.46 of [Whitehea...
pm2.47 389 Theorem *2.47 of [Whitehea...
pm2.48 390 Theorem *2.48 of [Whitehea...
pm2.49 391 Theorem *2.49 of [Whitehea...
pm2.67-2 392 Slight generalization of T...
pm2.67 393 Theorem *2.67 of [Whitehea...
pm2.25 394 Theorem *2.25 of [Whitehea...
biorf 395 A wff is equivalent to its...
biortn 396 A wff is equivalent to its...
biorfi 397 A wff is equivalent to its...
pm2.621 398 Theorem *2.621 of [Whitehe...
pm2.62 399 Theorem *2.62 of [Whitehea...
pm2.68 400 Theorem *2.68 of [Whitehea...
dfor2 401 Logical 'or' expressed in ...
imor 402 Implication in terms of di...
imori 403 Infer disjunction from imp...
imorri 404 Infer implication from dis...
exmid 405 Law of excluded middle, al...
exmidd 406 Law of excluded middle in ...
pm2.1 407 Theorem *2.1 of [Whitehead...
pm2.13 408 Theorem *2.13 of [Whitehea...
pm4.62 409 Theorem *4.62 of [Whitehea...
pm4.66 410 Theorem *4.66 of [Whitehea...
pm4.63 411 Theorem *4.63 of [Whitehea...
imnan 412 Express implication in ter...
imnani 413 Express implication in ter...
iman 414 Express implication in ter...
annim 415 Express conjunction in ter...
pm4.61 416 Theorem *4.61 of [Whitehea...
pm4.65 417 Theorem *4.65 of [Whitehea...
pm4.67 418 Theorem *4.67 of [Whitehea...
imp 419 Importation inference. (C...
impcom 420 Importation inference with...
imp3a 421 Importation deduction. (C...
imp31 422 An importation inference. ...
imp32 423 An importation inference. ...
ex 424 Exportation inference. (T...
expcom 425 Exportation inference with...
exp3a 426 Exportation deduction. (C...
expdimp 427 A deduction version of exp...
impancom 428 Mixed importation/commutat...
con3and 429 Variant of ~ con3d with im...
pm2.01da 430 Deduction based on reducti...
pm2.18da 431 Deduction based on reducti...
pm3.3 432 Theorem *3.3 (Exp) of [Whi...
pm3.31 433 Theorem *3.31 (Imp) of [Wh...
impexp 434 Import-export theorem. Pa...
pm3.2 435 Join antecedents with conj...
pm3.21 436 Join antecedents with conj...
pm3.22 437 Theorem *3.22 of [Whitehea...
ancom 438 Commutative law for conjun...
ancomd 439 Commutation of conjuncts i...
ancoms 440 Inference commuting conjun...
ancomsd 441 Deduction commuting conjun...
pm3.2i 442 Infer conjunction of premi...
pm3.43i 443 Nested conjunction of ante...
simpl 444 Elimination of a conjunct....
simpli 445 Inference eliminating a co...
simpld 446 Deduction eliminating a co...
simplbi 447 Deduction eliminating a co...
simpr 448 Elimination of a conjunct....
simpri 449 Inference eliminating a co...
simprd 450 Deduction eliminating a co...
simprbi 451 Deduction eliminating a co...
adantr 452 Inference adding a conjunc...
adantl 453 Inference adding a conjunc...
adantld 454 Deduction adding a conjunc...
adantrd 455 Deduction adding a conjunc...
mpan9 456 Modus ponens conjoining di...
syldan 457 A syllogism deduction with...
sylan 458 A syllogism inference. (C...
sylanb 459 A syllogism inference. (C...
sylanbr 460 A syllogism inference. (C...
sylan2 461 A syllogism inference. (C...
sylan2b 462 A syllogism inference. (C...
sylan2br 463 A syllogism inference. (C...
syl2an 464 A double syllogism inferen...
syl2anr 465 A double syllogism inferen...
syl2anb 466 A double syllogism inferen...
syl2anbr 467 A double syllogism inferen...
syland 468 A syllogism deduction. (C...
sylan2d 469 A syllogism deduction. (C...
syl2and 470 A syllogism deduction. (C...
biimpa 471 Inference from a logical e...
biimpar 472 Inference from a logical e...
biimpac 473 Inference from a logical e...
biimparc 474 Inference from a logical e...
ianor 475 Negated conjunction in ter...
anor 476 Conjunction in terms of di...
ioran 477 Negated disjunction in ter...
pm4.52 478 Theorem *4.52 of [Whitehea...
pm4.53 479 Theorem *4.53 of [Whitehea...
pm4.54 480 Theorem *4.54 of [Whitehea...
pm4.55 481 Theorem *4.55 of [Whitehea...
pm4.56 482 Theorem *4.56 of [Whitehea...
oran 483 Disjunction in terms of co...
pm4.57 484 Theorem *4.57 of [Whitehea...
pm3.1 485 Theorem *3.1 of [Whitehead...
pm3.11 486 Theorem *3.11 of [Whitehea...
pm3.12 487 Theorem *3.12 of [Whitehea...
pm3.13 488 Theorem *3.13 of [Whitehea...
pm3.14 489 Theorem *3.14 of [Whitehea...
iba 490 Introduction of antecedent...
ibar 491 Introduction of antecedent...
biantru 492 A wff is equivalent to its...
biantrur 493 A wff is equivalent to its...
biantrud 494 A wff is equivalent to its...
biantrurd 495 A wff is equivalent to its...
jaao 496 Inference conjoining and d...
jaoa 497 Inference disjoining and c...
pm3.44 498 Theorem *3.44 of [Whitehea...
jao 499 Disjunction of antecedents...
pm1.2 500 Axiom *1.2 of [WhiteheadRu...
oridm 501 Idempotent law for disjunc...
pm4.25 502 Theorem *4.25 of [Whitehea...
orim12i 503 Disjoin antecedents and co...
orim1i 504 Introduce disjunct to both...
orim2i 505 Introduce disjunct to both...
orbi2i 506 Inference adding a left di...
orbi1i 507 Inference adding a right d...
orbi12i 508 Infer the disjunction of t...
pm1.5 509 Axiom *1.5 (Assoc) of [Whi...
or12 510 Swap two disjuncts. (Cont...
orass 511 Associative law for disjun...
pm2.31 512 Theorem *2.31 of [Whitehea...
pm2.32 513 Theorem *2.32 of [Whitehea...
or32 514 A rearrangement of disjunc...
or4 515 Rearrangement of 4 disjunc...
or42 516 Rearrangement of 4 disjunc...
orordi 517 Distribution of disjunctio...
orordir 518 Distribution of disjunctio...
jca 519 Deduce conjunction of the ...
jcad 520 Deduction conjoining the c...
jca31 521 Join three consequents. (...
jca32 522 Join three consequents. (...
jcai 523 Deduction replacing implic...
jctil 524 Inference conjoining a the...
jctir 525 Inference conjoining a the...
jctl 526 Inference conjoining a the...
jctr 527 Inference conjoining a the...
jctild 528 Deduction conjoining a the...
jctird 529 Deduction conjoining a the...
ancl 530 Conjoin antecedent to left...
anclb 531 Conjoin antecedent to left...
pm5.42 532 Theorem *5.42 of [Whitehea...
ancr 533 Conjoin antecedent to righ...
ancrb 534 Conjoin antecedent to righ...
ancli 535 Deduction conjoining antec...
ancri 536 Deduction conjoining antec...
ancld 537 Deduction conjoining antec...
ancrd 538 Deduction conjoining antec...
anc2l 539 Conjoin antecedent to left...
anc2r 540 Conjoin antecedent to righ...
anc2li 541 Deduction conjoining antec...
anc2ri 542 Deduction conjoining antec...
pm3.41 543 Theorem *3.41 of [Whitehea...
pm3.42 544 Theorem *3.42 of [Whitehea...
pm3.4 545 Conjunction implies implic...
pm4.45im 546 Conjunction with implicati...
anim12d 547 Conjoin antecedents and co...
anim1d 548 Add a conjunct to right of...
anim2d 549 Add a conjunct to left of ...
anim12i 550 Conjoin antecedents and co...
anim12ci 551 Variant of ~ anim12i with ...
anim1i 552 Introduce conjunct to both...
anim2i 553 Introduce conjunct to both...
anim12ii 554 Conjoin antecedents and co...
prth 555 Conjoin antecedents and co...
pm2.3 556 Theorem *2.3 of [Whitehead...
pm2.41 557 Theorem *2.41 of [Whitehea...
pm2.42 558 Theorem *2.42 of [Whitehea...
pm2.4 559 Theorem *2.4 of [Whitehead...
pm2.65da 560 Deduction rule for proof b...
pm4.44 561 Theorem *4.44 of [Whitehea...
pm4.14 562 Theorem *4.14 of [Whitehea...
pm3.37 563 Theorem *3.37 (Transp) of ...
nan 564 Theorem to move a conjunct...
pm4.15 565 Theorem *4.15 of [Whitehea...
pm4.78 566 Implication distributes ov...
pm4.79 567 Theorem *4.79 of [Whitehea...
pm4.87 568 Theorem *4.87 of [Whitehea...
pm3.33 569 Theorem *3.33 (Syll) of [W...
pm3.34 570 Theorem *3.34 (Syll) of [W...
pm3.35 571 Conjunctive detachment. T...
pm5.31 572 Theorem *5.31 of [Whitehea...
imp4a 573 An importation inference. ...
imp4b 574 An importation inference. ...
imp4c 575 An importation inference. ...
imp4d 576 An importation inference. ...
imp41 577 An importation inference. ...
imp42 578 An importation inference. ...
imp43 579 An importation inference. ...
imp44 580 An importation inference. ...
imp45 581 An importation inference. ...
imp5a 582 An importation inference. ...
imp5d 583 An importation inference. ...
imp5g 584 An importation inference. ...
imp55 585 An importation inference. ...
imp511 586 An importation inference. ...
expimpd 587 Exportation followed by a ...
exp31 588 An exportation inference. ...
exp32 589 An exportation inference. ...
exp4a 590 An exportation inference. ...
exp4b 591 An exportation inference. ...
exp4c 592 An exportation inference. ...
exp4d 593 An exportation inference. ...
exp41 594 An exportation inference. ...
exp42 595 An exportation inference. ...
exp43 596 An exportation inference. ...
exp44 597 An exportation inference. ...
exp45 598 An exportation inference. ...
expr 599 Export a wff from a right ...
exp5c 600 An exportation inference. ...
exp53 601 An exportation inference. ...
expl 602 Export a wff from a left c...
impr 603 Import a wff into a right ...
impl 604 Export a wff from a left c...
impac 605 Importation with conjuncti...
exbiri 606 Inference form of ~ exbir ...
simprbda 607 Deduction eliminating a co...
simplbda 608 Deduction eliminating a co...
simplbi2 609 Deduction eliminating a co...
dfbi2 610 A theorem similar to the s...
dfbi 611 Definition ~ df-bi rewritt...
pm4.71 612 Implication in terms of bi...
pm4.71r 613 Implication in terms of bi...
pm4.71i 614 Inference converting an im...
pm4.71ri 615 Inference converting an im...
pm4.71d 616 Deduction converting an im...
pm4.71rd 617 Deduction converting an im...
pm5.32 618 Distribution of implicatio...
pm5.32i 619 Distribution of implicatio...
pm5.32ri 620 Distribution of implicatio...
pm5.32d 621 Distribution of implicatio...
pm5.32rd 622 Distribution of implicatio...
pm5.32da 623 Distribution of implicatio...
biadan2 624 Add a conjunction to an eq...
pm4.24 625 Theorem *4.24 of [Whitehea...
anidm 626 Idempotent law for conjunc...
anidms 627 Inference from idempotent ...
anidmdbi 628 Conjunction idempotence wi...
anasss 629 Associative law for conjun...
anassrs 630 Associative law for conjun...
anass 631 Associative law for conjun...
sylanl1 632 A syllogism inference. (C...
sylanl2 633 A syllogism inference. (C...
sylanr1 634 A syllogism inference. (C...
sylanr2 635 A syllogism inference. (C...
sylani 636 A syllogism inference. (C...
sylan2i 637 A syllogism inference. (C...
syl2ani 638 A syllogism inference. (C...
sylan9 639 Nested syllogism inference...
sylan9r 640 Nested syllogism inference...
mtand 641 A modus tollens deduction....
mtord 642 A modus tollens deduction ...
syl2anc 643 Syllogism inference combin...
sylancl 644 Syllogism inference combin...
sylancr 645 Syllogism inference combin...
sylanbrc 646 Syllogism inference. (Con...
sylancb 647 A syllogism inference comb...
sylancbr 648 A syllogism inference comb...
sylancom 649 Syllogism inference with c...
mpdan 650 An inference based on modu...
mpancom 651 An inference based on modu...
mpan 652 An inference based on modu...
mpan2 653 An inference based on modu...
mp2an 654 An inference based on modu...
mp4an 655 An inference based on modu...
mpan2d 656 A deduction based on modus...
mpand 657 A deduction based on modus...
mpani 658 An inference based on modu...
mpan2i 659 An inference based on modu...
mp2ani 660 An inference based on modu...
mp2and 661 A deduction based on modus...
mpanl1 662 An inference based on modu...
mpanl2 663 An inference based on modu...
mpanl12 664 An inference based on modu...
mpanr1 665 An inference based on modu...
mpanr2 666 An inference based on modu...
mpanr12 667 An inference based on modu...
mpanlr1 668 An inference based on modu...
pm5.74da 669 Distribution of implicatio...
pm4.45 670 Theorem *4.45 of [Whitehea...
imdistan 671 Distribution of implicatio...
imdistani 672 Distribution of implicatio...
imdistanri 673 Distribution of implicatio...
imdistand 674 Distribution of implicatio...
imdistanda 675 Distribution of implicatio...
anbi2i 676 Introduce a left conjunct ...
anbi1i 677 Introduce a right conjunct...
anbi2ci 678 Variant of ~ anbi2i with c...
anbi12i 679 Conjoin both sides of two ...
anbi12ci 680 Variant of ~ anbi12i with ...
sylan9bb 681 Nested syllogism inference...
sylan9bbr 682 Nested syllogism inference...
orbi2d 683 Deduction adding a left di...
orbi1d 684 Deduction adding a right d...
anbi2d 685 Deduction adding a left co...
anbi1d 686 Deduction adding a right c...
orbi1 687 Theorem *4.37 of [Whitehea...
anbi1 688 Introduce a right conjunct...
anbi2 689 Introduce a left conjunct ...
bitr 690 Theorem *4.22 of [Whitehea...
orbi12d 691 Deduction joining two equi...
anbi12d 692 Deduction joining two equi...
pm5.3 693 Theorem *5.3 of [Whitehead...
pm5.61 694 Theorem *5.61 of [Whitehea...
adantll 695 Deduction adding a conjunc...
adantlr 696 Deduction adding a conjunc...
adantrl 697 Deduction adding a conjunc...
adantrr 698 Deduction adding a conjunc...
adantlll 699 Deduction adding a conjunc...
adantllr 700 Deduction adding a conjunc...
adantlrl 701 Deduction adding a conjunc...
adantlrr 702 Deduction adding a conjunc...
adantrll 703 Deduction adding a conjunc...
adantrlr 704 Deduction adding a conjunc...
adantrrl 705 Deduction adding a conjunc...
adantrrr 706 Deduction adding a conjunc...
ad2antrr 707 Deduction adding two conju...
ad2antlr 708 Deduction adding two conju...
ad2antrl 709 Deduction adding two conju...
ad2antll 710 Deduction adding conjuncts...
ad3antrrr 711 Deduction adding three con...
ad3antlr 712 Deduction adding three con...
ad4antr 713 Deduction adding 4 conjunc...
ad4antlr 714 Deduction adding 4 conjunc...
ad5antr 715 Deduction adding 5 conjunc...
ad5antlr 716 Deduction adding 5 conjunc...
ad6antr 717 Deduction adding 6 conjunc...
ad6antlr 718 Deduction adding 6 conjunc...
ad7antr 719 Deduction adding 7 conjunc...
ad7antlr 720 Deduction adding 7 conjunc...
ad8antr 721 Deduction adding 8 conjunc...
ad8antlr 722 Deduction adding 8 conjunc...
ad9antr 723 Deduction adding 9 conjunc...
ad9antlr 724 Deduction adding 9 conjunc...
ad10antr 725 Deduction adding 10 conjun...
ad10antlr 726 Deduction adding 10 conjun...
ad2ant2l 727 Deduction adding two conju...
ad2ant2r 728 Deduction adding two conju...
ad2ant2lr 729 Deduction adding two conju...
ad2ant2rl 730 Deduction adding two conju...
simpll 731 Simplification of a conjun...
simplr 732 Simplification of a conjun...
simprl 733 Simplification of a conjun...
simprr 734 Simplification of a conjun...
simplll 735 Simplification of a conjun...
simpllr 736 Simplification of a conjun...
simplrl 737 Simplification of a conjun...
simplrr 738 Simplification of a conjun...
simprll 739 Simplification of a conjun...
simprlr 740 Simplification of a conjun...
simprrl 741 Simplification of a conjun...
simprrr 742 Simplification of a conjun...
simp-4l 743 Simplification of a conjun...
simp-4r 744 Simplification of a conjun...
simp-5l 745 Simplification of a conjun...
simp-5r 746 Simplification of a conjun...
simp-6l 747 Simplification of a conjun...
simp-6r 748 Simplification of a conjun...
simp-7l 749 Simplification of a conjun...
simp-7r 750 Simplification of a conjun...
simp-8l 751 Simplification of a conjun...
simp-8r 752 Simplification of a conjun...
simp-9l 753 Simplification of a conjun...
simp-9r 754 Simplification of a conjun...
simp-10l 755 Simplification of a conjun...
simp-10r 756 Simplification of a conjun...
simp-11l 757 Simplification of a conjun...
simp-11r 758 Simplification of a conjun...
jaob 759 Disjunction of antecedents...
jaoian 760 Inference disjoining the a...
jaodan 761 Deduction disjoining the a...
mpjaodan 762 Eliminate a disjunction in...
pm4.77 763 Theorem *4.77 of [Whitehea...
pm2.63 764 Theorem *2.63 of [Whitehea...
pm2.64 765 Theorem *2.64 of [Whitehea...
pm2.61ian 766 Elimination of an antecede...
pm2.61dan 767 Elimination of an antecede...
pm2.61ddan 768 Elimination of two anteced...
pm2.61dda 769 Elimination of two anteced...
condan 770 Proof by contradiction. (...
abai 771 Introduce one conjunct as ...
pm5.53 772 Theorem *5.53 of [Whitehea...
an12 773 Swap two conjuncts. Note ...
an32 774 A rearrangement of conjunc...
an13 775 A rearrangement of conjunc...
an31 776 A rearrangement of conjunc...
an12s 777 Swap two conjuncts in ante...
ancom2s 778 Inference commuting a nest...
an13s 779 Swap two conjuncts in ante...
an32s 780 Swap two conjuncts in ante...
ancom1s 781 Inference commuting a nest...
an31s 782 Swap two conjuncts in ante...
anass1rs 783 Commutative-associative la...
anabs1 784 Absorption into embedded c...
anabs5 785 Absorption into embedded c...
anabs7 786 Absorption into embedded c...
anabsan 787 Absorption of antecedent w...
anabss1 788 Absorption of antecedent i...
anabss4 789 Absorption of antecedent i...
anabss5 790 Absorption of antecedent i...
anabsi5 791 Absorption of antecedent i...
anabsi6 792 Absorption of antecedent i...
anabsi7 793 Absorption of antecedent i...
anabsi8 794 Absorption of antecedent i...
anabss7 795 Absorption of antecedent i...
anabsan2 796 Absorption of antecedent w...
anabss3 797 Absorption of antecedent i...
an4 798 Rearrangement of 4 conjunc...
an42 799 Rearrangement of 4 conjunc...
an4s 800 Inference rearranging 4 co...
an42s 801 Inference rearranging 4 co...
anandi 802 Distribution of conjunctio...
anandir 803 Distribution of conjunctio...
anandis 804 Inference that undistribut...
anandirs 805 Inference that undistribut...
impbida 806 Deduce an equivalence from...
pm3.48 807 Theorem *3.48 of [Whitehea...
pm3.45 808 Theorem *3.45 (Fact) of [W...
im2anan9 809 Deduction joining nested i...
im2anan9r 810 Deduction joining nested i...
anim12dan 811 Conjoin antecedents and co...
orim12d 812 Disjoin antecedents and co...
orim1d 813 Disjoin antecedents and co...
orim2d 814 Disjoin antecedents and co...
orim2 815 Axiom *1.6 (Sum) of [White...
pm2.38 816 Theorem *2.38 of [Whitehea...
pm2.36 817 Theorem *2.36 of [Whitehea...
pm2.37 818 Theorem *2.37 of [Whitehea...
pm2.73 819 Theorem *2.73 of [Whitehea...
pm2.74 820 Theorem *2.74 of [Whitehea...
orimdi 821 Disjunction distributes ov...
pm2.76 822 Theorem *2.76 of [Whitehea...
pm2.75 823 Theorem *2.75 of [Whitehea...
pm2.8 824 Theorem *2.8 of [Whitehead...
pm2.81 825 Theorem *2.81 of [Whitehea...
pm2.82 826 Theorem *2.82 of [Whitehea...
pm2.85 827 Theorem *2.85 of [Whitehea...
pm3.2ni 828 Infer negated disjunction ...
orabs 829 Absorption of redundant in...
oranabs 830 Absorb a disjunct into a c...
pm5.1 831 Two propositions are equiv...
pm5.21 832 Two propositions are equiv...
pm3.43 833 Theorem *3.43 (Comp) of [W...
jcab 834 Distributive law for impli...
ordi 835 Distributive law for disju...
ordir 836 Distributive law for disju...
pm4.76 837 Theorem *4.76 of [Whitehea...
andi 838 Distributive law for conju...
andir 839 Distributive law for conju...
orddi 840 Double distributive law fo...
anddi 841 Double distributive law fo...
pm4.39 842 Theorem *4.39 of [Whitehea...
pm4.38 843 Theorem *4.38 of [Whitehea...
bi2anan9 844 Deduction joining two equi...
bi2anan9r 845 Deduction joining two equi...
bi2bian9 846 Deduction joining two bico...
pm4.72 847 Implication in terms of bi...
imimorb 848 Simplify an implication be...
pm5.33 849 Theorem *5.33 of [Whitehea...
pm5.36 850 Theorem *5.36 of [Whitehea...
bianabs 851 Absorb a hypothesis into t...
oibabs 852 Absorption of disjunction ...
pm3.24 853 Law of noncontradiction. ...
pm2.26 854 Theorem *2.26 of [Whitehea...
pm5.11 855 Theorem *5.11 of [Whitehea...
pm5.12 856 Theorem *5.12 of [Whitehea...
pm5.14 857 Theorem *5.14 of [Whitehea...
pm5.13 858 Theorem *5.13 of [Whitehea...
pm5.17 859 Theorem *5.17 of [Whitehea...
pm5.15 860 Theorem *5.15 of [Whitehea...
pm5.16 861 Theorem *5.16 of [Whitehea...
xor 862 Two ways to express "exclu...
nbi2 863 Two ways to express "exclu...
dfbi3 864 An alternate definition of...
pm5.24 865 Theorem *5.24 of [Whitehea...
xordi 866 Conjunction distributes ov...
biort 867 A wff disjoined with truth...
pm5.55 868 Theorem *5.55 of [Whitehea...
pm5.21nd 869 Eliminate an antecedent im...
pm5.35 870 Theorem *5.35 of [Whitehea...
pm5.54 871 Theorem *5.54 of [Whitehea...
baib 872 Move conjunction outside o...
baibr 873 Move conjunction outside o...
rbaib 874 Move conjunction outside o...
rbaibr 875 Move conjunction outside o...
baibd 876 Move conjunction outside o...
rbaibd 877 Move conjunction outside o...
pm5.44 878 Theorem *5.44 of [Whitehea...
pm5.6 879 Conjunction in antecedent ...
orcanai 880 Change disjunction in cons...
intnan 881 Introduction of conjunct i...
intnanr 882 Introduction of conjunct i...
intnand 883 Introduction of conjunct i...
intnanrd 884 Introduction of conjunct i...
mpbiran 885 Detach truth from conjunct...
mpbiran2 886 Detach truth from conjunct...
mpbir2an 887 Detach a conjunction of tr...
mpbi2and 888 Detach a conjunction of tr...
mpbir2and 889 Detach a conjunction of tr...
pm5.62 890 Theorem *5.62 of [Whitehea...
pm5.63 891 Theorem *5.63 of [Whitehea...
bianfi 892 A wff conjoined with false...
bianfd 893 A wff conjoined with false...
pm4.43 894 Theorem *4.43 of [Whitehea...
pm4.82 895 Theorem *4.82 of [Whitehea...
pm4.83 896 Theorem *4.83 of [Whitehea...
pclem6 897 Negation inferred from emb...
biantr 898 A transitive law of equiva...
orbidi 899 Disjunction distributes ov...
biluk 900 Lukasiewicz's shortest axi...
pm5.7 901 Disjunction distributes ov...
bigolden 902 Dijkstra-Scholten's Golden...
pm5.71 903 Theorem *5.71 of [Whitehea...
pm5.75 904 Theorem *5.75 of [Whitehea...
bimsc1 905 Removal of conjunct from o...
4exmid 906 The disjunction of the fou...
ecase2d 907 Deduction for elimination ...
ecase3 908 Inference for elimination ...
ecase 909 Inference for elimination ...
ecase3d 910 Deduction for elimination ...
ecased 911 Deduction for elimination ...
ecase3ad 912 Deduction for elimination ...
ccase 913 Inference for combining ca...
ccased 914 Deduction for combining ca...
ccase2 915 Inference for combining ca...
4cases 916 Inference eliminating two ...
4casesdan 917 Deduction eliminating two ...
niabn 918 Miscellaneous inference re...
dedlem0a 919 Lemma for an alternate ver...
dedlem0b 920 Lemma for an alternate ver...
dedlema 921 Lemma for weak deduction t...
dedlemb 922 Lemma for weak deduction t...
elimh 923 Hypothesis builder for wea...
dedt 924 The weak deduction theorem...
con3th 925 Contraposition. Theorem *...
consensus 926 The consensus theorem. Th...
pm4.42 927 Theorem *4.42 of [Whitehea...
ninba 928 Miscellaneous inference re...
prlem1 929 A specialized lemma for se...
prlem2 930 A specialized lemma for se...
oplem1 931 A specialized lemma for se...
rnlem 932 Lemma used in construction...
dn1 933 A single axiom for Boolean...
jaoi2 934 Inference removing a negat...
3orass 939 Associative law for triple...
3anass 940 Associative law for triple...
3anrot 941 Rotation law for triple co...
3orrot 942 Rotation law for triple di...
3ancoma 943 Commutation law for triple...
3orcoma 944 Commutation law for triple...
3ancomb 945 Commutation law for triple...
3orcomb 946 Commutation law for triple...
3anrev 947 Reversal law for triple co...
3anan32 948 Convert triple conjunction...
3anan12 949 Convert triple conjunction...
3anor 950 Triple conjunction express...
3ianor 951 Negated triple conjunction...
3ioran 952 Negated triple disjunction...
3oran 953 Triple disjunction in term...
3simpa 954 Simplification of triple c...
3simpb 955 Simplification of triple c...
3simpc 956 Simplification of triple c...
simp1 957 Simplification of triple c...
simp2 958 Simplification of triple c...
simp3 959 Simplification of triple c...
simpl1 960 Simplification rule. (Con...
simpl2 961 Simplification rule. (Con...
simpl3 962 Simplification rule. (Con...
simpr1 963 Simplification rule. (Con...
simpr2 964 Simplification rule. (Con...
simpr3 965 Simplification rule. (Con...
simp1i 966 Infer a conjunct from a tr...
simp2i 967 Infer a conjunct from a tr...
simp3i 968 Infer a conjunct from a tr...
simp1d 969 Deduce a conjunct from a t...
simp2d 970 Deduce a conjunct from a t...
simp3d 971 Deduce a conjunct from a t...
simp1bi 972 Deduce a conjunct from a t...
simp2bi 973 Deduce a conjunct from a t...
simp3bi 974 Deduce a conjunct from a t...
3adant1 975 Deduction adding a conjunc...
3adant2 976 Deduction adding a conjunc...
3adant3 977 Deduction adding a conjunc...
3ad2ant1 978 Deduction adding conjuncts...
3ad2ant2 979 Deduction adding conjuncts...
3ad2ant3 980 Deduction adding conjuncts...
simp1l 981 Simplification of triple c...
simp1r 982 Simplification of triple c...
simp2l 983 Simplification of triple c...
simp2r 984 Simplification of triple c...
simp3l 985 Simplification of triple c...
simp3r 986 Simplification of triple c...
simp11 987 Simplification of doubly t...
simp12 988 Simplification of doubly t...
simp13 989 Simplification of doubly t...
simp21 990 Simplification of doubly t...
simp22 991 Simplification of doubly t...
simp23 992 Simplification of doubly t...
simp31 993 Simplification of doubly t...
simp32 994 Simplification of doubly t...
simp33 995 Simplification of doubly t...
simpll1 996 Simplification of conjunct...
simpll2 997 Simplification of conjunct...
simpll3 998 Simplification of conjunct...
simplr1 999 Simplification of conjunct...
simplr2 1000 Simplification of conjunct...
simplr3 1001 Simplification of conjunct...
simprl1 1002 Simplification of conjunct...
simprl2 1003 Simplification of conjunct...
simprl3 1004 Simplification of conjunct...
simprr1 1005 Simplification of conjunct...
simprr2 1006 Simplification of conjunct...
simprr3 1007 Simplification of conjunct...
simpl1l 1008 Simplification of conjunct...
simpl1r 1009 Simplification of conjunct...
simpl2l 1010 Simplification of conjunct...
simpl2r 1011 Simplification of conjunct...
simpl3l 1012 Simplification of conjunct...
simpl3r 1013 Simplification of conjunct...
simpr1l 1014 Simplification of conjunct...
simpr1r 1015 Simplification of conjunct...
simpr2l 1016 Simplification of conjunct...
simpr2r 1017 Simplification of conjunct...
simpr3l 1018 Simplification of conjunct...
simpr3r 1019 Simplification of conjunct...
simp1ll 1020 Simplification of conjunct...
simp1lr 1021 Simplification of conjunct...
simp1rl 1022 Simplification of conjunct...
simp1rr 1023 Simplification of conjunct...
simp2ll 1024 Simplification of conjunct...
simp2lr 1025 Simplification of conjunct...
simp2rl 1026 Simplification of conjunct...
simp2rr 1027 Simplification of conjunct...
simp3ll 1028 Simplification of conjunct...
simp3lr 1029 Simplification of conjunct...
simp3rl 1030 Simplification of conjunct...
simp3rr 1031 Simplification of conjunct...
simpl11 1032 Simplification of conjunct...
simpl12 1033 Simplification of conjunct...
simpl13 1034 Simplification of conjunct...
simpl21 1035 Simplification of conjunct...
simpl22 1036 Simplification of conjunct...
simpl23 1037 Simplification of conjunct...
simpl31 1038 Simplification of conjunct...
simpl32 1039 Simplification of conjunct...
simpl33 1040 Simplification of conjunct...
simpr11 1041 Simplification of conjunct...
simpr12 1042 Simplification of conjunct...
simpr13 1043 Simplification of conjunct...
simpr21 1044 Simplification of conjunct...
simpr22 1045 Simplification of conjunct...
simpr23 1046 Simplification of conjunct...
simpr31 1047 Simplification of conjunct...
simpr32 1048 Simplification of conjunct...
simpr33 1049 Simplification of conjunct...
simp1l1 1050 Simplification of conjunct...
simp1l2 1051 Simplification of conjunct...
simp1l3 1052 Simplification of conjunct...
simp1r1 1053 Simplification of conjunct...
simp1r2 1054 Simplification of conjunct...
simp1r3 1055 Simplification of conjunct...
simp2l1 1056 Simplification of conjunct...
simp2l2 1057 Simplification of conjunct...
simp2l3 1058 Simplification of conjunct...
simp2r1 1059 Simplification of conjunct...
simp2r2 1060 Simplification of conjunct...
simp2r3 1061 Simplification of conjunct...
simp3l1 1062 Simplification of conjunct...
simp3l2 1063 Simplification of conjunct...
simp3l3 1064 Simplification of conjunct...
simp3r1 1065 Simplification of conjunct...
simp3r2 1066 Simplification of conjunct...
simp3r3 1067 Simplification of conjunct...
simp11l 1068 Simplification of conjunct...
simp11r 1069 Simplification of conjunct...
simp12l 1070 Simplification of conjunct...
simp12r 1071 Simplification of conjunct...
simp13l 1072 Simplification of conjunct...
simp13r 1073 Simplification of conjunct...
simp21l 1074 Simplification of conjunct...
simp21r 1075 Simplification of conjunct...
simp22l 1076 Simplification of conjunct...
simp22r 1077 Simplification of conjunct...
simp23l 1078 Simplification of conjunct...
simp23r 1079 Simplification of conjunct...
simp31l 1080 Simplification of conjunct...
simp31r 1081 Simplification of conjunct...
simp32l 1082 Simplification of conjunct...
simp32r 1083 Simplification of conjunct...
simp33l 1084 Simplification of conjunct...
simp33r 1085 Simplification of conjunct...
simp111 1086 Simplification of conjunct...
simp112 1087 Simplification of conjunct...
simp113 1088 Simplification of conjunct...
simp121 1089 Simplification of conjunct...
simp122 1090 Simplification of conjunct...
simp123 1091 Simplification of conjunct...
simp131 1092 Simplification of conjunct...
simp132 1093 Simplification of conjunct...
simp133 1094 Simplification of conjunct...
simp211 1095 Simplification of conjunct...
simp212 1096 Simplification of conjunct...
simp213 1097 Simplification of conjunct...
simp221 1098 Simplification of conjunct...
simp222 1099 Simplification of conjunct...
simp223 1100 Simplification of conjunct...
simp231 1101 Simplification of conjunct...
simp232 1102 Simplification of conjunct...
simp233 1103 Simplification of conjunct...
simp311 1104 Simplification of conjunct...
simp312 1105 Simplification of conjunct...
simp313 1106 Simplification of conjunct...
simp321 1107 Simplification of conjunct...
simp322 1108 Simplification of conjunct...
simp323 1109 Simplification of conjunct...
simp331 1110 Simplification of conjunct...
simp332 1111 Simplification of conjunct...
simp333 1112 Simplification of conjunct...
3adantl1 1113 Deduction adding a conjunc...
3adantl2 1114 Deduction adding a conjunc...
3adantl3 1115 Deduction adding a conjunc...
3adantr1 1116 Deduction adding a conjunc...
3adantr2 1117 Deduction adding a conjunc...
3adantr3 1118 Deduction adding a conjunc...
3ad2antl1 1119 Deduction adding conjuncts...
3ad2antl2 1120 Deduction adding conjuncts...
3ad2antl3 1121 Deduction adding conjuncts...
3ad2antr1 1122 Deduction adding conjuncts...
3ad2antr2 1123 Deduction adding conjuncts...
3ad2antr3 1124 Deduction adding conjuncts...
3anibar 1125 Remove a hypothesis from t...
3mix1 1126 Introduction in triple dis...
3mix2 1127 Introduction in triple dis...
3mix3 1128 Introduction in triple dis...
3mix1i 1129 Introduction in triple dis...
3mix2i 1130 Introduction in triple dis...
3mix3i 1131 Introduction in triple dis...
3pm3.2i 1132 Infer conjunction of premi...
pm3.2an3 1133 ~ pm3.2 for a triple conju...
3jca 1134 Join consequents with conj...
3jcad 1135 Deduction conjoining the c...
mpbir3an 1136 Detach a conjunction of tr...
mpbir3and 1137 Detach a conjunction of tr...
syl3anbrc 1138 Syllogism inference. (Con...
3anim123i 1139 Join antecedents and conse...
3anim1i 1140 Add two conjuncts to antec...
3anim3i 1141 Add two conjuncts to antec...
3anbi123i 1142 Join 3 biconditionals with...
3orbi123i 1143 Join 3 biconditionals with...
3anbi1i 1144 Inference adding two conju...
3anbi2i 1145 Inference adding two conju...
3anbi3i 1146 Inference adding two conju...
3imp 1147 Importation inference. (C...
3impa 1148 Importation from double to...
3impb 1149 Importation from double to...
3impia 1150 Importation to triple conj...
3impib 1151 Importation to triple conj...
3exp 1152 Exportation inference. (C...
3expa 1153 Exportation from triple to...
3expb 1154 Exportation from triple to...
3expia 1155 Exportation from triple co...
3expib 1156 Exportation from triple co...
3com12 1157 Commutation in antecedent....
3com13 1158 Commutation in antecedent....
3com23 1159 Commutation in antecedent....
3coml 1160 Commutation in antecedent....
3comr 1161 Commutation in antecedent....
3adant3r1 1162 Deduction adding a conjunc...
3adant3r2 1163 Deduction adding a conjunc...
3adant3r3 1164 Deduction adding a conjunc...
3an1rs 1165 Swap conjuncts. (Contribu...
3imp1 1166 Importation to left triple...
3impd 1167 Importation deduction for ...
3imp2 1168 Importation to right tripl...
3exp1 1169 Exportation from left trip...
3expd 1170 Exportation deduction for ...
3exp2 1171 Exportation from right tri...
exp5o 1172 A triple exportation infer...
exp516 1173 A triple exportation infer...
exp520 1174 A triple exportation infer...
3anassrs 1175 Associative law for conjun...
3adant1l 1176 Deduction adding a conjunc...
3adant1r 1177 Deduction adding a conjunc...
3adant2l 1178 Deduction adding a conjunc...
3adant2r 1179 Deduction adding a conjunc...
3adant3l 1180 Deduction adding a conjunc...
3adant3r 1181 Deduction adding a conjunc...
syl12anc 1182 Syllogism combined with co...
syl21anc 1183 Syllogism combined with co...
syl3anc 1184 Syllogism combined with co...
syl22anc 1185 Syllogism combined with co...
syl13anc 1186 Syllogism combined with co...
syl31anc 1187 Syllogism combined with co...
syl112anc 1188 Syllogism combined with co...
syl121anc 1189 Syllogism combined with co...
syl211anc 1190 Syllogism combined with co...
syl23anc 1191 Syllogism combined with co...
syl32anc 1192 Syllogism combined with co...
syl122anc 1193 Syllogism combined with co...
syl212anc 1194 Syllogism combined with co...
syl221anc 1195 Syllogism combined with co...
syl113anc 1196 Syllogism combined with co...
syl131anc 1197 Syllogism combined with co...
syl311anc 1198 Syllogism combined with co...
syl33anc 1199 Syllogism combined with co...
syl222anc 1200 Syllogism combined with co...
syl123anc 1201 Syllogism combined with co...
syl132anc 1202 Syllogism combined with co...
syl213anc 1203 Syllogism combined with co...
syl231anc 1204 Syllogism combined with co...
syl312anc 1205 Syllogism combined with co...
syl321anc 1206 Syllogism combined with co...
syl133anc 1207 Syllogism combined with co...
syl313anc 1208 Syllogism combined with co...
syl331anc 1209 Syllogism combined with co...
syl223anc 1210 Syllogism combined with co...
syl232anc 1211 Syllogism combined with co...
syl322anc 1212 Syllogism combined with co...
syl233anc 1213 Syllogism combined with co...
syl323anc 1214 Syllogism combined with co...
syl332anc 1215 Syllogism combined with co...
syl333anc 1216 A syllogism inference comb...
syl3an1 1217 A syllogism inference. (C...
syl3an2 1218 A syllogism inference. (C...
syl3an3 1219 A syllogism inference. (C...
syl3an1b 1220 A syllogism inference. (C...
syl3an2b 1221 A syllogism inference. (C...
syl3an3b 1222 A syllogism inference. (C...
syl3an1br 1223 A syllogism inference. (C...
syl3an2br 1224 A syllogism inference. (C...
syl3an3br 1225 A syllogism inference. (C...
syl3an 1226 A triple syllogism inferen...
syl3anb 1227 A triple syllogism inferen...
syl3anbr 1228 A triple syllogism inferen...
syld3an3 1229 A syllogism inference. (C...
syld3an1 1230 A syllogism inference. (C...
syld3an2 1231 A syllogism inference. (C...
syl3anl1 1232 A syllogism inference. (C...
syl3anl2 1233 A syllogism inference. (C...
syl3anl3 1234 A syllogism inference. (C...
syl3anl 1235 A triple syllogism inferen...
syl3anr1 1236 A syllogism inference. (C...
syl3anr2 1237 A syllogism inference. (C...
syl3anr3 1238 A syllogism inference. (C...
3impdi 1239 Importation inference (und...
3impdir 1240 Importation inference (und...
3anidm12 1241 Inference from idempotent ...
3anidm13 1242 Inference from idempotent ...
3anidm23 1243 Inference from idempotent ...
3ori 1244 Infer implication from tri...
3jao 1245 Disjunction of 3 anteceden...
3jaob 1246 Disjunction of 3 anteceden...
3jaoi 1247 Disjunction of 3 anteceden...
3jaod 1248 Disjunction of 3 anteceden...
3jaoian 1249 Disjunction of 3 anteceden...
3jaodan 1250 Disjunction of 3 anteceden...
3jaao 1251 Inference conjoining and d...
syl3an9b 1252 Nested syllogism inference...
3orbi123d 1253 Deduction joining 3 equiva...
3anbi123d 1254 Deduction joining 3 equiva...
3anbi12d 1255 Deduction conjoining and a...
3anbi13d 1256 Deduction conjoining and a...
3anbi23d 1257 Deduction conjoining and a...
3anbi1d 1258 Deduction adding conjuncts...
3anbi2d 1259 Deduction adding conjuncts...
3anbi3d 1260 Deduction adding conjuncts...
3anim123d 1261 Deduction joining 3 implic...
3orim123d 1262 Deduction joining 3 implic...
an6 1263 Rearrangement of 6 conjunc...
3an6 1264 Analog of ~ an4 for triple...
3or6 1265 Analog of ~ or4 for triple...
mp3an1 1266 An inference based on modu...
mp3an2 1267 An inference based on modu...
mp3an3 1268 An inference based on modu...
mp3an12 1269 An inference based on modu...
mp3an13 1270 An inference based on modu...
mp3an23 1271 An inference based on modu...
mp3an1i 1272 An inference based on modu...
mp3anl1 1273 An inference based on modu...
mp3anl2 1274 An inference based on modu...
mp3anl3 1275 An inference based on modu...
mp3anr1 1276 An inference based on modu...
mp3anr2 1277 An inference based on modu...
mp3anr3 1278 An inference based on modu...
mp3an 1279 An inference based on modu...
mpd3an3 1280 An inference based on modu...
mpd3an23 1281 An inference based on modu...
mp3and 1282 A deduction based on modus...
biimp3a 1283 Infer implication from a l...
biimp3ar 1284 Infer implication from a l...
3anandis 1285 Inference that undistribut...
3anandirs 1286 Inference that undistribut...
ecase23d 1287 Deduction for elimination ...
3ecase 1288 Inference for elimination ...
3bior1fd 1289 A disjunction is equivalen...
3bior1fand 1290 A disjunction is equivalen...
3bior2fd 1291 A wff is equivalent to its...
3biant1d 1292 A conjunction is equivalen...
nanan 1295 Write 'and' in terms of 'n...
nancom 1296 The 'nand' operator commut...
nannan 1297 Lemma for handling nested ...
nanim 1298 Show equivalence between i...
nannot 1299 Show equivalence between n...
nanbi 1300 Show equivalence between t...
nanbi1 1301 Introduce a right anti-con...
nanbi2 1302 Introduce a left anti-conj...
nanbi12 1303 Join two logical equivalen...
nanbi1i 1304 Introduce a right anti-con...
nanbi2i 1305 Introduce a left anti-conj...
nanbi12i 1306 Join two logical equivalen...
nanbi1d 1307 Introduce a right anti-con...
nanbi2d 1308 Introduce a left anti-conj...
nanbi12d 1309 Join two logical equivalen...
xnor 1312 Two ways to write XNOR. (C...
xorcom 1313 ` \/_ ` is commutative. (...
xorass 1314 ` \/_ ` is associative. (...
excxor 1315 This tautology shows that ...
xor2 1316 Two ways to express "exclu...
xorneg1 1317 ` \/_ ` is negated under n...
xorneg2 1318 ` \/_ ` is negated under n...
xorneg 1319 ` \/_ ` is unchanged under...
xorbi12i 1320 Equality property for XOR....
xorbi12d 1321 Equality property for XOR....
trujust 1324 Soundness justification th...
tru 1327 ` T. ` is provable. (Cont...
fal 1328 ` F. ` is refutable. (Con...
trud 1329 Eliminate ` T. ` as an ant...
tbtru 1330 If something is true, it o...
nbfal 1331 If something is not true, ...
bitru 1332 A theorem is equivalent to...
bifal 1333 A contradiction is equival...
falim 1334 ` F. ` implies anything. ...
falimd 1335 ` F. ` implies anything. ...
a1tru 1336 Anything implies ` T. ` . ...
truan 1337 True can be removed from a...
dfnot 1338 Given falsum, we can defin...
inegd 1339 Negation introduction rule...
efald 1340 Deduction based on reducti...
pm2.21fal 1341 If a wff and its negation ...
truantru 1342 A ` /\ ` identity. (Contr...
truanfal 1343 A ` /\ ` identity. (Contr...
falantru 1344 A ` /\ ` identity. (Contr...
falanfal 1345 A ` /\ ` identity. (Contr...
truortru 1346 A ` \/ ` identity. (Contr...
truorfal 1347 A ` \/ ` identity. (Contr...
falortru 1348 A ` \/ ` identity. (Contr...
falorfal 1349 A ` \/ ` identity. (Contr...
truimtru 1350 A ` -> ` identity. (Contr...
truimfal 1351 A ` -> ` identity. (Contr...
falimtru 1352 A ` -> ` identity. (Contr...
falimfal 1353 A ` -> ` identity. (Contr...
nottru 1354 A ` -. ` identity. (Contr...
notfal 1355 A ` -. ` identity. (Contr...
trubitru 1356 A ` <-> ` identity. (Cont...
trubifal 1357 A ` <-> ` identity. (Cont...
falbitru 1358 A ` <-> ` identity. (Cont...
falbifal 1359 A ` <-> ` identity. (Cont...
trunantru 1360 A ` -/\ ` identity. (Cont...
trunanfal 1361 A ` -/\ ` identity. (Cont...
falnantru 1362 A ` -/\ ` identity. (Cont...
falnanfal 1363 A ` -/\ ` identity. (Cont...
truxortru 1364 A ` \/_ ` identity. (Cont...
truxorfal 1365 A ` \/_ ` identity. (Cont...
falxortru 1366 A ` \/_ ` identity. (Cont...
falxorfal 1367 A ` \/_ ` identity. (Cont...
ee22 1368 Virtual deduction rule ~ e...
ee12an 1369 ~ e12an without virtual de...
ee23 1370 ~ e23 without virtual dedu...
exbir 1371 Exportation implication al...
3impexp 1372 ~ impexp with a 3-conjunct...
3impexpbicom 1373 ~ 3impexp with bicondition...
3impexpbicomi 1374 Deduction form of ~ 3impex...
ancomsimp 1375 Closed form of ~ ancoms . ...
exp3acom3r 1376 Export and commute anteced...
exp3acom23g 1377 Implication form of ~ exp3...
exp3acom23 1378 The exportation deduction ...
simplbi2comg 1379 Implication form of ~ simp...
simplbi2com 1380 A deduction eliminating a ...
ee21 1381 ~ e21 without virtual dedu...
ee10 1382 ~ e10 without virtual dedu...
ee02 1383 ~ e02 without virtual dedu...
hadbi123d 1388 Equality theorem for half ...
cadbi123d 1389 Equality theorem for adder...
hadbi123i 1390 Equality theorem for half ...
cadbi123i 1391 Equality theorem for adder...
hadass 1392 Associative law for triple...
hadbi 1393 The half adder is the same...
hadcoma 1394 Commutative law for triple...
hadcomb 1395 Commutative law for triple...
hadrot 1396 Rotation law for triple XO...
cador 1397 Write the adder carry in d...
cadan 1398 Write the adder carry in c...
hadnot 1399 The half adder distributes...
cadnot 1400 The adder carry distribute...
cadcoma 1401 Commutative law for adder ...
cadcomb 1402 Commutative law for adder ...
cadrot 1403 Rotation law for adder car...
cad1 1404 If one parameter is true, ...
cad11 1405 If two parameters are true...
cad0 1406 If one parameter is false,...
cadtru 1407 Rotation law for adder car...
had1 1408 If the first parameter is ...
had0 1409 If the first parameter is ...
meredith 1410 Carew Meredith's sole axio...
axmeredith 1411 Alias for ~ meredith which...
merlem1 1413 Step 3 of Meredith's proof...
merlem2 1414 Step 4 of Meredith's proof...
merlem3 1415 Step 7 of Meredith's proof...
merlem4 1416 Step 8 of Meredith's proof...
merlem5 1417 Step 11 of Meredith's proo...
merlem6 1418 Step 12 of Meredith's proo...
merlem7 1419 Between steps 14 and 15 of...
merlem8 1420 Step 15 of Meredith's proo...
merlem9 1421 Step 18 of Meredith's proo...
merlem10 1422 Step 19 of Meredith's proo...
merlem11 1423 Step 20 of Meredith's proo...
merlem12 1424 Step 28 of Meredith's proo...
merlem13 1425 Step 35 of Meredith's proo...
luk-1 1426 1 of 3 axioms for proposit...
luk-2 1427 2 of 3 axioms for proposit...
luk-3 1428 3 of 3 axioms for proposit...
luklem1 1429 Used to rederive standard ...
luklem2 1430 Used to rederive standard ...
luklem3 1431 Used to rederive standard ...
luklem4 1432 Used to rederive standard ...
luklem5 1433 Used to rederive standard ...
luklem6 1434 Used to rederive standard ...
luklem7 1435 Used to rederive standard ...
luklem8 1436 Used to rederive standard ...
ax1 1437 Standard propositional axi...
ax2 1438 Standard propositional axi...
ax3 1439 Standard propositional axi...
nic-dfim 1440 Define implication in term...
nic-dfneg 1441 Define negation in terms o...
nic-mp 1442 Derive Nicod's rule of mod...
nic-mpALT 1443 A direct proof of ~ nic-mp...
nic-ax 1444 Nicod's axiom derived from...
nic-axALT 1445 A direct proof of ~ nic-ax...
nic-imp 1446 Inference for ~ nic-mp usi...
nic-idlem1 1447 Lemma for ~ nic-id . (Con...
nic-idlem2 1448 Lemma for ~ nic-id . Infe...
nic-id 1449 Theorem ~ id expressed wit...
nic-swap 1450 ` -/\ ` is symmetric. (Co...
nic-isw1 1451 Inference version of ~ nic...
nic-isw2 1452 Inference for swapping nes...
nic-iimp1 1453 Inference version of ~ nic...
nic-iimp2 1454 Inference version of ~ nic...
nic-idel 1455 Inference to remove the tr...
nic-ich 1456 Chained inference. (Contr...
nic-idbl 1457 Double the terms. Since d...
nic-bijust 1458 For nic-* definitions, the...
nic-bi1 1459 Inference to extract one s...
nic-bi2 1460 Inference to extract the o...
nic-stdmp 1461 Derive the standard modus ...
nic-luk1 1462 Proof of ~ luk-1 from ~ ni...
nic-luk2 1463 Proof of ~ luk-2 from ~ ni...
nic-luk3 1464 Proof of ~ luk-3 from ~ ni...
lukshef-ax1 1465 This alternative axiom for...
lukshefth1 1466 Lemma for ~ renicax . (Co...
lukshefth2 1467 Lemma for ~ renicax . (Co...
renicax 1468 A rederivation of ~ nic-ax...
tbw-bijust 1469 Justification for ~ tbw-ne...
tbw-negdf 1470 The definition of negation...
tbw-ax1 1471 The first of four axioms i...
tbw-ax2 1472 The second of four axioms ...
tbw-ax3 1473 The third of four axioms i...
tbw-ax4 1474 The fourth of four axioms ...
tbwsyl 1475 Used to rederive the Lukas...
tbwlem1 1476 Used to rederive the Lukas...
tbwlem2 1477 Used to rederive the Lukas...
tbwlem3 1478 Used to rederive the Lukas...
tbwlem4 1479 Used to rederive the Lukas...
tbwlem5 1480 Used to rederive the Lukas...
re1luk1 1481 ~ luk-1 derived from the T...
re1luk2 1482 ~ luk-2 derived from the T...
re1luk3 1483 ~ luk-3 derived from the T...
merco1 1484 A single axiom for proposi...
merco1lem1 1485 Used to rederive the Tarsk...
retbwax4 1486 ~ tbw-ax4 rederived from ~...
retbwax2 1487 ~ tbw-ax2 rederived from ~...
merco1lem2 1488 Used to rederive the Tarsk...
merco1lem3 1489 Used to rederive the Tarsk...
merco1lem4 1490 Used to rederive the Tarsk...
merco1lem5 1491 Used to rederive the Tarsk...
merco1lem6 1492 Used to rederive the Tarsk...
merco1lem7 1493 Used to rederive the Tarsk...
retbwax3 1494 ~ tbw-ax3 rederived from ~...
merco1lem8 1495 Used to rederive the Tarsk...
merco1lem9 1496 Used to rederive the Tarsk...
merco1lem10 1497 Used to rederive the Tarsk...
merco1lem11 1498 Used to rederive the Tarsk...
merco1lem12 1499 Used to rederive the Tarsk...
merco1lem13 1500 Used to rederive the Tarsk...
merco1lem14 1501 Used to rederive the Tarsk...
merco1lem15 1502 Used to rederive the Tarsk...
merco1lem16 1503 Used to rederive the Tarsk...
merco1lem17 1504 Used to rederive the Tarsk...
merco1lem18 1505 Used to rederive the Tarsk...
retbwax1 1506 ~ tbw-ax1 rederived from ~...
merco2 1507 A single axiom for proposi...
mercolem1 1508 Used to rederive the Tarsk...
mercolem2 1509 Used to rederive the Tarsk...
mercolem3 1510 Used to rederive the Tarsk...
mercolem4 1511 Used to rederive the Tarsk...
mercolem5 1512 Used to rederive the Tarsk...
mercolem6 1513 Used to rederive the Tarsk...
mercolem7 1514 Used to rederive the Tarsk...
mercolem8 1515 Used to rederive the Tarsk...
re1tbw1 1516 ~ tbw-ax1 rederived from ~...
re1tbw2 1517 ~ tbw-ax2 rederived from ~...
re1tbw3 1518 ~ tbw-ax3 rederived from ~...
re1tbw4 1519 ~ tbw-ax4 rederived from ~...
rb-bijust 1520 Justification for ~ rb-imd...
rb-imdf 1521 The definition of implicat...
anmp 1522 Modus ponens for ` \/ ` ` ...
rb-ax1 1523 The first of four axioms i...
rb-ax2 1524 The second of four axioms ...
rb-ax3 1525 The third of four axioms i...
rb-ax4 1526 The fourth of four axioms ...
rbsyl 1527 Used to rederive the Lukas...
rblem1 1528 Used to rederive the Lukas...
rblem2 1529 Used to rederive the Lukas...
rblem3 1530 Used to rederive the Lukas...
rblem4 1531 Used to rederive the Lukas...
rblem5 1532 Used to rederive the Lukas...
rblem6 1533 Used to rederive the Lukas...
rblem7 1534 Used to rederive the Lukas...
re1axmp 1535 ~ ax-mp derived from Russe...
re2luk1 1536 ~ luk-1 derived from Russe...
re2luk2 1537 ~ luk-2 derived from Russe...
re2luk3 1538 ~ luk-3 derived from Russe...
mpto1 1539 Modus ponendo tollens 1, o...
mpto2 1540 Modus ponendo tollens 2, o...
mpto2OLD 1541 Obsolete version of ~ mpto...
mtp-xor 1542 Modus tollendo ponens (ori...
mtp-xorOLD 1543 Obsolete version of ~ mtp-...
mtp-or 1544 Modus tollendo ponens (inc...
mtp-orOLD 1545 Obsolete version of ~ mtp-...
alnex 1549 Theorem 19.7 of [Margaris]...
gen2 1553 Generalization applied twi...
mpg 1554 Modus ponens combined with...
mpgbi 1555 Modus ponens on biconditio...
mpgbir 1556 Modus ponens on biconditio...
nfi 1557 Deduce that ` x ` is not f...
hbth 1558 No variable is (effectivel...
nfth 1559 No variable is (effectivel...
nftru 1560 The true constant has no f...
nex 1561 Generalization rule for ne...
nfnth 1562 No variable is (effectivel...
alim 1564 Theorem 19.20 of [Margaris...
alimi 1565 Inference quantifying both...
2alimi 1566 Inference doubly quantifyi...
al2imi 1567 Inference quantifying ante...
alanimi 1568 Variant of ~ al2imi with c...
alimdh 1569 Deduction from Theorem 19....
albi 1570 Theorem 19.15 of [Margaris...
alrimih 1571 Inference from Theorem 19....
albii 1572 Inference adding universal...
2albii 1573 Inference adding two unive...
hbxfrbi 1574 A utility lemma to transfe...
nfbii 1575 Equality theorem for not-f...
nfxfr 1576 A utility lemma to transfe...
nfxfrd 1577 A utility lemma to transfe...
alex 1578 Theorem 19.6 of [Margaris]...
2nalexn 1579 Part of theorem *11.5 in [...
exnal 1580 Theorem 19.14 of [Margaris...
exim 1581 Theorem 19.22 of [Margaris...
eximi 1582 Inference adding existenti...
2eximi 1583 Inference adding two exist...
eximii 1584 Inference associated with ...
alinexa 1585 A transformation of quanti...
alexn 1586 A relationship between two...
2exnexn 1587 Theorem *11.51 in [Whitehe...
exbi 1588 Theorem 19.18 of [Margaris...
exbii 1589 Inference adding existenti...
2exbii 1590 Inference adding two exist...
3exbii 1591 Inference adding 3 existen...
exanali 1592 A transformation of quanti...
exancom 1593 Commutation of conjunction...
alrimdh 1594 Deduction from Theorem 19....
eximdh 1595 Deduction from Theorem 19....
nexdh 1596 Deduction for generalizati...
albidh 1597 Formula-building rule for ...
exbidh 1598 Formula-building rule for ...
exsimpl 1599 Simplification of an exist...
19.26 1600 Theorem 19.26 of [Margaris...
19.26-2 1601 Theorem 19.26 of [Margaris...
19.26-3an 1602 Theorem 19.26 of [Margaris...
19.29 1603 Theorem 19.29 of [Margaris...
19.29r 1604 Variation of Theorem 19.29...
19.29r2 1605 Variation of Theorem 19.29...
19.29x 1606 Variation of Theorem 19.29...
19.35 1607 Theorem 19.35 of [Margaris...
19.35i 1608 Inference from Theorem 19....
19.35ri 1609 Inference from Theorem 19....
19.25 1610 Theorem 19.25 of [Margaris...
19.30 1611 Theorem 19.30 of [Margaris...
19.43 1612 Theorem 19.43 of [Margaris...
19.43OLD 1613 Obsolete proof of ~ 19.43 ...
19.33 1614 Theorem 19.33 of [Margaris...
19.33b 1615 The antecedent provides a ...
19.40 1616 Theorem 19.40 of [Margaris...
19.40-2 1617 Theorem *11.42 in [Whitehe...
albiim 1618 Split a biconditional and ...
2albiim 1619 Split a biconditional and ...
exintrbi 1620 Add/remove a conjunct in t...
exintr 1621 Introduce a conjunct in th...
alsyl 1622 Theorem *10.3 in [Whitehea...
a17d 1624 ~ ax-17 with antecedent. ...
ax17e 1625 A rephrasing of ~ ax-17 us...
nfv 1626 If ` x ` is not present in...
nfvd 1627 ~ nfv with antecedent. Us...
alimdv 1628 Deduction from Theorem 19....
eximdv 1629 Deduction from Theorem 19....
2alimdv 1630 Deduction from Theorem 19....
2eximdv 1631 Deduction from Theorem 19....
albidv 1632 Formula-building rule for ...
exbidv 1633 Formula-building rule for ...
2albidv 1634 Formula-building rule for ...
2exbidv 1635 Formula-building rule for ...
3exbidv 1636 Formula-building rule for ...
4exbidv 1637 Formula-building rule for ...
alrimiv 1638 Inference from Theorem 19....
alrimivv 1639 Inference from Theorem 19....
alrimdv 1640 Deduction from Theorem 19....
exlimiv 1641 Inference from Theorem 19....
exlimivv 1642 Inference from Theorem 19....
exlimdv 1643 Deduction from Theorem 19....
exlimdvv 1644 Deduction from Theorem 19....
exlimddv 1645 Existential elimination ru...
nfdv 1646 Apply the definition of no...
2ax17 1647 Quantification of two vari...
weq 1650 Extend wff definition to i...
equs3 1651 Lemma used in proofs of su...
speimfw 1652 Specialization, with addit...
spimfw 1653 Specialization, with addit...
ax11i 1654 Inference that has ~ ax-11...
sbequ2 1657 An equality theorem for su...
sbequ2OLD 1658 Obsolete proof of ~ sbequ2...
sb1 1659 One direction of a simplif...
sbimi 1660 Infer substitution into an...
sbbii 1661 Infer substitution into bo...
ax9v 1663 Axiom B7 of [Tarski] p. 75...
a9ev 1664 At least one individual ex...
exiftru 1665 A companion rule to ax-gen...
exiftruOLD 1666 Obsolete proof of ~ exiftr...
19.2 1667 Theorem 19.2 of [Margaris]...
19.8w 1668 Weak version of ~ 19.8a . ...
19.39 1669 Theorem 19.39 of [Margaris...
19.24 1670 Theorem 19.24 of [Margaris...
19.34 1671 Theorem 19.34 of [Margaris...
19.9v 1672 Special case of Theorem 19...
19.3v 1673 Special case of Theorem 19...
spvw 1674 Version of ~ sp when ` x `...
spimeh 1675 Existential introduction, ...
spimw 1676 Specialization. Lemma 8 o...
spimvw 1677 Specialization. Lemma 8 o...
spnfw 1678 Weak version of ~ sp . Us...
sptruw 1679 Version of ~ sp when ` ph ...
spfalw 1680 Version of ~ sp when ` ph ...
cbvaliw 1681 Change bound variable. Us...
cbvalivw 1682 Change bound variable. Us...
equid 1684 Identity law for equality....
equidOLD 1685 Obsolete proof of ~ equid ...
nfequid 1686 Bound-variable hypothesis ...
equcomi 1687 Commutative law for equali...
equcom 1688 Commutative law for equali...
equcoms 1689 An inference commuting equ...
equtr 1690 A transitive law for equal...
equtrr 1691 A transitive law for equal...
equequ1 1692 An equivalence law for equ...
equequ1OLD 1693 Obsolete version of ~ eque...
equequ2 1694 An equivalence law for equ...
stdpc6 1695 One of the two equality ax...
equtr2 1696 A transitive law for equal...
ax12b 1697 Two equivalent ways of exp...
ax12bOLD 1698 Obsolete version of ~ ax12...
spfw 1699 Weak version of ~ sp . Us...
spnfwOLD 1700 Weak version of ~ sp . Us...
19.8wOLD 1701 Obsolete version of ~ 19.8...
spw 1702 Weak version of specializa...
spwOLD 1703 Obsolete proof of ~ spw as...
spvwOLD 1704 Obsolete version of ~ spvw...
19.3vOLD 1705 Obsolete version of ~ 19.3...
19.9vOLD 1706 Obsolete version of ~ 19.9...
exlimivOLD 1707 Obsolete version of ~ exli...
spfalwOLD 1708 Obsolete proof of ~ spfalw...
19.2OLD 1709 Obsolete version of ~ 19.2...
cbvalw 1710 Change bound variable. Us...
cbvalvw 1711 Change bound variable. Us...
cbvalvwOLD 1712 Change bound variable. Us...
cbvexvw 1713 Change bound variable. Us...
alcomiw 1714 Weak version of ~ alcom . ...
hbn1fw 1715 Weak version of ~ ax-6 fro...
hbn1fwOLD 1716 Obsolete proof of ~ hbn1fw...
hbn1w 1717 Weak version of ~ hbn1 . ...
hba1w 1718 Weak version of ~ hba1 . ...
hbe1w 1719 Weak version of ~ hbe1 . ...
hbalw 1720 Weak version of ~ hbal . ...
wel 1722 Extend wff definition to i...
elequ1 1724 An identity law for the no...
elequ2 1726 An identity law for the no...
ax9dgen 1727 Tarski's system uses the w...
ax6w 1728 Weak version of ~ ax-6 fro...
ax7w 1729 Weak version of ~ ax-7 fro...
ax7dgen 1730 Degenerate instance of ~ a...
ax11wlem 1731 Lemma for weak version of ...
ax11w 1732 Weak version of ~ ax-11 fr...
ax11dgen 1733 Degenerate instance of ~ a...
ax11wdemo 1734 Example of an application ...
ax12w 1735 Weak version (principal in...
ax12dgen1 1736 Degenerate instance of ~ a...
ax12dgen2 1737 Degenerate instance of ~ a...
ax12dgen3 1738 Degenerate instance of ~ a...
ax12dgen4 1739 Degenerate instance of ~ a...
hbn1 1741 ` x ` is not free in ` -. ...
hbe1 1742 ` x ` is not free in ` E. ...
nfe1 1743 ` x ` is not free in ` E. ...
modal-5 1744 The analog in our predicat...
a7s 1746 Swap quantifiers in an ant...
hbal 1747 If ` x ` is not free in ` ...
alcom 1748 Theorem 19.5 of [Margaris]...
alrot3 1749 Theorem *11.21 in [Whitehe...
alrot4 1750 Rotate 4 universal quantif...
hbald 1751 Deduction form of bound-va...
excom 1752 Theorem 19.11 of [Margaris...
excomim 1753 One direction of Theorem 1...
excom13 1754 Swap 1st and 3rd existenti...
exrot3 1755 Rotate existential quantif...
exrot4 1756 Rotate existential quantif...
19.8a 1758 If a wff is true, it is tr...
sp 1759 Specialization. A univers...
spOLD 1760 Obsolete proof of ~ sp as ...
ax5o 1761 Show that the original axi...
ax6o 1762 Show that the original axi...
a6e 1763 Abbreviated version of ~ a...
modal-b 1764 The analog in our predicat...
spi 1765 Inference rule reversing g...
sps 1766 Generalization of antecede...
spsd 1767 Deduction generalizing ant...
19.8aOLD 1768 If a wff is true, it is tr...
19.2g 1769 Theorem 19.2 of [Margaris]...
19.21bi 1770 Inference from Theorem 19....
19.23bi 1771 Inference from Theorem 19....
nexr 1772 Inference from ~ 19.8a . ...
nfr 1773 Consequence of the definit...
nfri 1774 Consequence of the definit...
nfrd 1775 Consequence of the definit...
alimd 1776 Deduction from Theorem 19....
alrimi 1777 Inference from Theorem 19....
nfd 1778 Deduce that ` x ` is not f...
nfdh 1779 Deduce that ` x ` is not f...
alrimdd 1780 Deduction from Theorem 19....
alrimd 1781 Deduction from Theorem 19....
eximd 1782 Deduction from Theorem 19....
nexd 1783 Deduction for generalizati...
albid 1784 Formula-building rule for ...
exbid 1785 Formula-building rule for ...
nfbidf 1786 An equality theorem for ef...
19.3 1787 A wff may be quantified wi...
19.9ht 1788 A closed version of ~ 19.9...
19.9t 1789 A closed version of ~ 19.9...
19.9h 1790 A wff may be existentially...
19.9hOLD 1791 Obsolete proof of ~ 19.9h ...
19.9d 1792 A deduction version of one...
19.9 1793 A wff may be existentially...
19.9OLD 1794 Obsolete proof of ~ 19.9 a...
hbnt 1795 Closed theorem version of ...
hbntOLD 1796 Obsolete proof of ~ hbnt a...
hbn 1797 If ` x ` is not free in ` ...
hbnOLD 1798 Obsolete proof of ~ hbn as...
19.9htOLD 1799 Obsolete proof of ~ 19.9ht...
hba1 1800 ` x ` is not free in ` A. ...
hba1OLD 1801 Obsolete proof of ~ hba1 a...
nfa1 1802 ` x ` is not free in ` A. ...
a5i 1803 Inference version of ~ ax5...
nfnf1 1804 ` x ` is not free in ` F/ ...
nfnd 1805 If in a context ` x ` is n...
nfndOLD 1806 Obsolete proof of ~ nfnd a...
nfn 1807 If ` x ` is not free in ` ...
19.38 1808 Theorem 19.38 of [Margaris...
19.21t 1809 Closed form of Theorem 19....
19.21 1810 Theorem 19.21 of [Margaris...
19.21h 1811 Theorem 19.21 of [Margaris...
stdpc5 1812 An axiom scheme of standar...
stdpc5OLD 1813 Obsolete proof of ~ stdpc5...
19.23t 1814 Closed form of Theorem 19....
19.23 1815 Theorem 19.23 of [Margaris...
19.23h 1816 Theorem 19.23 of [Margaris...
exlimi 1817 Inference from Theorem 19....
exlimih 1818 Inference from Theorem 19....
exlimihOLD 1819 Obsolete proof of ~ exlimi...
exlimd 1820 Deduction from Theorem 19....
exlimdOLD 1821 Obsolete proof of ~ exlimd...
exlimdh 1822 Deduction from Theorem 19....
nfimd 1823 If in a context ` x ` is n...
nfimdOLD 1824 Obsolete proof of ~ nfimd ...
hbim1 1825 A closed form of ~ hbim . ...
nfim1 1826 A closed form of ~ nfim . ...
nfim1OLD 1827 A closed form of ~ nfim . ...
nfim 1828 If ` x ` is not free in ` ...
nfimOLD 1829 If ` x ` is not free in ` ...
hbimd 1830 Deduction form of bound-va...
hbimdOLD 1831 Obsolete proof of ~ hbimd ...
hbim 1832 If ` x ` is not free in ` ...
hbimOLD 1833 Obsolete proof of ~ hbim a...
19.23tOLD 1834 Obsolete proof of ~ 19.23t...
19.23hOLD 1835 Obsolete proof of ~ 19.23h...
spimehOLD 1836 Obsolete proof of ~ spimeh...
19.27 1837 Theorem 19.27 of [Margaris...
19.28 1838 Theorem 19.28 of [Margaris...
nfand 1839 If in a context ` x ` is n...
nf3and 1840 Deduction form of bound-va...
nfan1 1841 A closed form of ~ nfan . ...
nfan 1842 If ` x ` is not free in ` ...
nfnan 1843 If ` x ` is not free in ` ...
nfanOLD 1844 Obsolete proof of ~ nfan a...
nf3an 1845 If ` x ` is not free in ` ...
hban 1846 If ` x ` is not free in ` ...
hbanOLD 1847 Obsolete proof of ~ hban a...
hb3an 1848 If ` x ` is not free in ` ...
hb3anOLD 1849 Obsolete proof of ~ hb3an ...
nfbid 1850 If in a context ` x ` is n...
nfbidOLD 1851 Obsolete proof of ~ nfbid ...
nfbi 1852 If ` x ` is not free in ` ...
nfbiOLD 1853 If ` x ` is not free in ` ...
nfor 1854 If ` x ` is not free in ` ...
nf3or 1855 If ` x ` is not free in ` ...
equsalhw 1856 Weaker version of ~ equsal...
equsalhwOLD 1857 Obsolete proof of ~ equsal...
19.21hOLD 1858 Obsolete proof of ~ 19.21h...
hbex 1859 If ` x ` is not free in ` ...
nfal 1860 If ` x ` is not free in ` ...
nfex 1861 If ` x ` is not free in ` ...
nfexOLD 1862 Obsolete proof of ~ nfex a...
nfnf 1863 If ` x ` is not free in ` ...
nfnfOLD 1864 Obsolete proof of ~ nfnf a...
19.12 1865 Theorem 19.12 of [Margaris...
19.12OLD 1866 Obsolete proof of ~ 19.12 ...
nfald 1867 If ` x ` is not free in ` ...
nfaldOLD 1868 Obsolete proof of ~ nfald ...
nfexd 1869 If ` x ` is not free in ` ...
nfa2 1870 Lemma 24 of [Monk2] p. 114...
nfia1 1871 Lemma 23 of [Monk2] p. 114...
dvelimhw 1872 Proof of ~ dvelimh without...
dvelimhwOLD 1873 Proof of ~ dvelimh without...
cbv3hv 1874 Lemma for ~ ax10 . Simila...
cbv3hvOLD 1875 Obsolete proof of ~ cbv3hv...
19.9tOLD 1876 Obsolete proof of ~ 19.9t ...
excomimOLD 1877 Obsolete proof of ~ excomi...
excomOLD 1878 Obsolete proof of ~ excom ...
19.16 1879 Theorem 19.16 of [Margaris...
19.17 1880 Theorem 19.17 of [Margaris...
19.19 1881 Theorem 19.19 of [Margaris...
19.21tOLD 1882 Obsolete proof of ~ 19.21t...
19.21-2 1883 Theorem 19.21 of [Margaris...
19.21bbi 1884 Inference removing double ...
nf2 1885 An alternative definition ...
nf3 1886 An alternative definition ...
nf4 1887 Variable ` x ` is effectiv...
19.36 1888 Theorem 19.36 of [Margaris...
19.36i 1889 Inference from Theorem 19....
19.37 1890 Theorem 19.37 of [Margaris...
19.38OLD 1891 Obsolete proof of ~ 19.38 ...
19.32 1892 Theorem 19.32 of [Margaris...
19.31 1893 Theorem 19.31 of [Margaris...
19.44 1894 Theorem 19.44 of [Margaris...
19.45 1895 Theorem 19.45 of [Margaris...
19.41 1896 Theorem 19.41 of [Margaris...
19.41OLD 1897 Obsolete proof of ~ 19.41 ...
19.42 1898 Theorem 19.42 of [Margaris...
exan 1899 Place a conjunct in the sc...
exanOLD 1900 Obsolete proof of ~ exan a...
hbnd 1901 Deduction form of bound-va...
aaan 1902 Rearrange universal quanti...
eeor 1903 Rearrange existential quan...
qexmid 1904 Quantified "excluded middl...
equs5a 1905 A property related to subs...
equs5e 1906 A property related to subs...
equs5eOLD 1907 Obsolete proof of ~ equs5e...
exlimdd 1908 Existential elimination ru...
19.21v 1909 Special case of Theorem 19...
19.23v 1910 Special case of Theorem 19...
19.23vv 1911 Theorem 19.23 of [Margaris...
pm11.53 1912 Theorem *11.53 in [Whitehe...
19.27v 1913 Theorem 19.27 of [Margaris...
19.28v 1914 Theorem 19.28 of [Margaris...
19.36v 1915 Special case of Theorem 19...
19.36aiv 1916 Inference from Theorem 19....
19.12vv 1917 Special case of ~ 19.12 wh...
19.37v 1918 Special case of Theorem 19...
19.37aiv 1919 Inference from Theorem 19....
19.41v 1920 Special case of Theorem 19...
19.41vv 1921 Theorem 19.41 of [Margaris...
19.41vvv 1922 Theorem 19.41 of [Margaris...
19.41vvvv 1923 Theorem 19.41 of [Margaris...
19.42v 1924 Special case of Theorem 19...
exdistr 1925 Distribution of existentia...
19.42vv 1926 Theorem 19.42 of [Margaris...
19.42vvv 1927 Theorem 19.42 of [Margaris...
exdistr2 1928 Distribution of existentia...
3exdistr 1929 Distribution of existentia...
4exdistr 1930 Distribution of existentia...
4exdistrOLD 1931 Obsolete proof of ~ 4exdis...
eean 1932 Rearrange existential quan...
eeanv 1933 Rearrange existential quan...
eeeanv 1934 Rearrange existential quan...
eeeanvOLD 1935 Obsolete proof of ~ eeeanv...
ee4anv 1936 Rearrange existential quan...
nexdv 1937 Deduction for generalizati...
stdpc7 1938 One of the two equality ax...
sbequ1 1939 An equality theorem for su...
sbequ12 1940 An equality theorem for su...
sbequ12r 1941 An equality theorem for su...
sbequ12a 1942 An equality theorem for su...
sbid 1943 An identity theorem for su...
sb4a 1944 A version of ~ sb4 that do...
sb4e 1945 One direction of a simplif...
ax12v 1947 A weaker version of ~ ax-1...
a9e 1948 At least one individual ex...
ax9 1949 Theorem showing that ~ ax-...
ax9o 1950 Show that the original axi...
equs4 1951 Lemma used in proofs of su...
equs4OLD 1952 Obsolete proof of ~ equs4 ...
spimt 1953 Closed theorem form of ~ s...
spimtOLD 1954 Obsolete proof of ~ spimt ...
spim 1955 Specialization, using impl...
spimOLD 1956 Obsolete proof of ~ spim a...
spimeOLD 1957 Obsolete proof of ~ spime ...
spimed 1958 Deduction version of ~ spi...
spimedOLD 1959 Obsolete proof of ~ spimed...
spime 1960 Existential introduction, ...
spimv 1961 A version of ~ spim with a...
spimev 1962 Distinct-variable version ...
spv 1963 Specialization, using impl...
spei 1964 Inference from existential...
speivOLD 1965 Obsolete proof of ~ spei a...
equsal 1966 A useful equivalence relat...
equsalOLD 1967 Obsolete proof of ~ equsal...
equsalh 1968 A useful equivalence relat...
equsex 1969 A useful equivalence relat...
equsexOLD 1970 Obsolete proof of ~ equsex...
equsexh 1971 A useful equivalence relat...
ax12olem1 1972 Lemma for ~ ax12o and ~ dv...
ax12olem2 1973 Lemma for ~ ax12o and ~ dv...
ax12olem3 1974 Lemma for ~ ax12o and ~ dv...
ax12olem4 1975 Lemma for ~ ax12o . (Cont...
ax12o 1976 Derive set.mm's original ~...
ax12olem1OLD 1977 Obsolete proof of ~ ax12oO...
ax12olem2OLD 1978 Obsolete proof of ~ ax12oO...
ax12olem3OLD 1979 Obsolete proof of ~ ax12oO...
ax12olem4OLD 1980 Obsolete proof of ~ ax12oO...
ax12olem5OLD 1981 Obsolete proof of ~ ax12oO...
ax12olem6OLD 1982 Obsolete proof of ~ ax12oO...
ax12olem7OLD 1983 Obsolete proof of ~ ax12oO...
ax12oOLD 1984 Obsolete proof of ~ ax12oO...
ax12 1985 Derive ~ ax-12 from ~ ax12...
ax12OLD 1986 Obsolete proof of ~ ax12 a...
dveeq1 1987 Quantifier introduction wh...
ax10lem1 1988 Lemma for ~ ax10 . Change...
ax10lem2 1989 Lemma for ~ ax10 . Change...
ax10lem3 1990 Lemma for ~ ax10 . Simila...
ax10 1991 Derive set.mm's original ~...
ax10lem2OLD 1992 Obsolete proof of a lemma ...
ax10lem3OLD 1993 Obsolete proof of a lemma ...
dvelimvOLD 1994 Obsolete proof of ~ dvelim...
dveeq2OLD 1995 Obsolete proof of ~ dveeq2...
ax10lem4OLD 1996 Obsolete proof of ~ ax10le...
ax10lem5OLD 1997 Obsolete proof of ~ ax10le...
ax10OLD 1998 Obsolete proof of ~ ax10 a...
ax9OLD 1999 Obsolete proof of ~ ax9 as...
a9eOLD 2000 Obsolete proof of ~ a9e as...
ax10o 2001 Show that ~ ax-10o can be ...
aecom 2002 Commutation law for identi...
aecoms 2003 A commutation rule for ide...
naecoms 2004 A commutation rule for dis...
hbae 2005 All variables are effectiv...
nfae 2006 All variables are effectiv...
hbnae 2007 All variables are effectiv...
nfnae 2008 All variables are effectiv...
hbnaes 2009 Rule that applies ~ hbnae ...
aevlem1 2010 Lemma for ~ aev and ~ a16g...
aev 2011 A "distinctor elimination"...
a16g 2012 Generalization of ~ ax16 ....
a16gOLD 2013 Obsolete proof of ~ a16g a...
nfeqf 2014 A variable is effectively ...
dvelimh 2015 Version of ~ dvelim withou...
dvelimhOLD 2016 Obslete proof of ~ dvelimh...
dvelimv 2017 Similar to ~ dvelim with f...
dveeq1OLD 2018 Obsolete proof of ~ dveeq1...
dveeq2 2019 Quantifier introduction wh...
dral2 2020 Formula-building lemma for...
dral2OLD 2021 Formula-building lemma for...
dral1 2022 Formula-building lemma for...
dral1OLD 2023 Obsolete proof of ~ dral1 ...
drex1 2024 Formula-building lemma for...
drex2 2025 Formula-building lemma for...
drnf1 2026 Formula-building lemma for...
drnf2 2027 Formula-building lemma for...
exdistrf 2028 Distribution of existentia...
nfald2 2029 Variation on ~ nfald which...
nfexd2 2030 Variation on ~ nfexd which...
cbv1h 2031 Rule used to change bound ...
cbv1 2032 Rule used to change bound ...
cbv2h 2033 Rule used to change bound ...
cbv2 2034 Rule used to change bound ...
cbv3 2035 Rule used to change bound ...
cbv3h 2036 Rule used to change bound ...
cbval 2037 Rule used to change bound ...
cbvex 2038 Rule used to change bound ...
chvar 2039 Implicit substitution of `...
equvini 2040 A variable introduction la...
equviniOLD 2041 Obsolete proof of ~ equvin...
equveli 2042 A variable elimination law...
equveliOLD 2043 Obsolete proof of ~ equvel...
equs45f 2044 Two ways of expressing sub...
ax11v2 2045 Recovery of ~ ax-11o from ...
ax11a2 2046 Derive ~ ax-11o from a hyp...
ax11o 2047 Derivation of set.mm's ori...
ax11b 2048 A bidirectional version of...
equs5 2049 Lemma used in proofs of su...
dvelimf 2050 Version of ~ dvelimv witho...
equvin 2051 A variable introduction la...
cbvalv 2052 Rule used to change bound ...
cbvexv 2053 Rule used to change bound ...
cbval2 2054 Rule used to change bound ...
cbvex2 2055 Rule used to change bound ...
cbval2v 2056 Rule used to change bound ...
cbvex2v 2057 Rule used to change bound ...
cbvald 2058 Deduction used to change b...
cbvexd 2059 Deduction used to change b...
cbvaldva 2060 Rule used to change the bo...
cbvexdva 2061 Rule used to change the bo...
cbvex4v 2062 Rule used to change bound ...
chvarv 2063 Implicit substitution of `...
cleljust 2064 When the class variables i...
cleljustALT 2065 When the class variables i...
dvelim 2066 This theorem can be used t...
dvelimnf 2067 Version of ~ dvelim using ...
dveel1 2068 Quantifier introduction wh...
dveel2 2069 Quantifier introduction wh...
ax15 2070 Axiom ~ ax-15 is redundant...
drsb1 2071 Formula-building lemma for...
sb2 2072 One direction of a simplif...
stdpc4 2073 The specialization axiom o...
sbft 2074 Substitution has no effect...
sbf 2075 Substitution for a variabl...
sbh 2076 Substitution for a variabl...
sbf2 2077 Substitution has no effect...
sb6x 2078 Equivalence involving subs...
nfs1f 2079 If ` x ` is not free in ` ...
sbequ5 2080 Substitution does not chan...
sbequ6 2081 Substitution does not chan...
sbt 2082 A substitution into a theo...
equsb1 2083 Substitution applied to an...
equsb2 2084 Substitution applied to an...
sbied 2085 Conversion of implicit sub...
sbiedv 2086 Conversion of implicit sub...
sbie 2087 Conversion of implicit sub...
sb6f 2088 Equivalence for substituti...
sb5f 2089 Equivalence for substituti...
hbsb2a 2090 Special case of a bound-va...
hbsb2e 2091 Special case of a bound-va...
hbsb3 2092 If ` y ` is not free in ` ...
nfs1 2093 If ` y ` is not free in ` ...
ax16 2094 Proof of older axiom ~ ax-...
ax16i 2095 Inference with ~ ax16 as i...
ax16ALT 2096 Alternate proof of ~ ax16 ...
ax16ALT2 2097 Alternate proof of ~ ax16 ...
a16gALT 2098 A generalization of axiom ...
a16gb 2099 A generalization of axiom ...
a16nf 2100 If ~ dtru is false, then t...
sb3 2101 One direction of a simplif...
sb4 2102 One direction of a simplif...
sb4b 2103 Simplified definition of s...
dfsb2 2104 An alternate definition of...
dfsb3 2105 An alternate definition of...
hbsb2 2106 Bound-variable hypothesis ...
nfsb2 2107 Bound-variable hypothesis ...
sbequi 2108 An equality theorem for su...
sbequ 2109 An equality theorem for su...
drsb2 2110 Formula-building lemma for...
sbn 2111 Negation inside and outsid...
sbi1 2112 Removal of implication fro...
sbi2 2113 Introduction of implicatio...
sbim 2114 Implication inside and out...
sbor 2115 Logical OR inside and outs...
sbrim 2116 Substitution with a variab...
sblim 2117 Substitution with a variab...
sban 2118 Conjunction inside and out...
sb3an 2119 Conjunction inside and out...
sbbi 2120 Equivalence inside and out...
sblbis 2121 Introduce left bicondition...
sbrbis 2122 Introduce right biconditio...
sbrbif 2123 Introduce right biconditio...
spsbe 2124 A specialization theorem. ...
spsbim 2125 Specialization of implicat...
spsbbi 2126 Specialization of bicondit...
sbbid 2127 Deduction substituting bot...
sbequ8 2128 Elimination of equality fr...
nfsb4t 2129 A variable not free remain...
nfsb4 2130 A variable not free remain...
dvelimdf 2131 Deduction form of ~ dvelim...
sbco 2132 A composition law for subs...
sbid2 2133 An identity law for substi...
sbidm 2134 An idempotent law for subs...
sbco2 2135 A composition law for subs...
sbco2d 2136 A composition law for subs...
sbco3 2137 A composition law for subs...
sbcom 2138 A commutativity law for su...
sb5rf 2139 Reversed substitution. (C...
sb6rf 2140 Reversed substitution. (C...
sb8 2141 Substitution of variable i...
sb8e 2142 Substitution of variable i...
sb9i 2143 Commutation of quantificat...
sb9 2144 Commutation of quantificat...
ax11v 2145 This is a version of ~ ax-...
ax11vALT 2146 Alternate proof of ~ ax11v...
sb56 2147 Two equivalent ways of exp...
sb6 2148 Equivalence for substituti...
sb5 2149 Equivalence for substituti...
equsb3lem 2150 Lemma for ~ equsb3 . (Con...
equsb3 2151 Substitution applied to an...
elsb3 2152 Substitution applied to an...
elsb4 2153 Substitution applied to an...
hbs1 2154 ` x ` is not free in ` [ y...
nfs1v 2155 ` x ` is not free in ` [ y...
sbhb 2156 Two ways of expressing " `...
sbnf2 2157 Two ways of expressing " `...
nfsb 2158 If ` z ` is not free in ` ...
hbsb 2159 If ` z ` is not free in ` ...
nfsbd 2160 Deduction version of ~ nfs...
2sb5 2161 Equivalence for double sub...
2sb6 2162 Equivalence for double sub...
sbcom2 2163 Commutativity law for subs...
pm11.07 2164 (Probably not) Axiom *11.0...
pm11.07OLD 2165 Obsolete proof of ~ pm11.0...
sb6a 2166 Equivalence for substituti...
2sb5rf 2167 Reversed double substituti...
2sb6rf 2168 Reversed double substituti...
sb7f 2169 This version of ~ dfsb7 do...
sb7h 2170 This version of ~ dfsb7 do...
dfsb7 2171 An alternate definition of...
sb10f 2172 Hao Wang's identity axiom ...
sbid2v 2173 An identity law for substi...
sbelx 2174 Elimination of substitutio...
sbel2x 2175 Elimination of double subs...
sbal1 2176 A theorem used in eliminat...
sbal 2177 Move universal quantifier ...
sbex 2178 Move existential quantifie...
sbalv 2179 Quantify with new variable...
exsb 2180 An equivalent expression f...
exsbOLD 2181 An equivalent expression f...
2exsb 2182 An equivalent expression f...
dvelimALT 2183 Version of ~ dvelim that d...
sbal2 2184 Move quantifier in and out...
ax4 2195 This theorem repeats ~ sp ...
ax5 2196 Rederivation of axiom ~ ax...
ax6 2197 Rederivation of axiom ~ ax...
ax9from9o 2198 Rederivation of axiom ~ ax...
hba1-o 2199 ` x ` is not free in ` A. ...
a5i-o 2200 Inference version of ~ ax-...
aecom-o 2201 Commutation law for identi...
aecoms-o 2202 A commutation rule for ide...
hbae-o 2203 All variables are effectiv...
dral1-o 2204 Formula-building lemma for...
ax11 2205 Rederivation of axiom ~ ax...
ax12from12o 2206 Derive ~ ax-12 from ~ ax-1...
ax17o 2207 Axiom to quantify a variab...
equid1 2208 Identity law for equality ...
sps-o 2209 Generalization of antecede...
hbequid 2210 Bound-variable hypothesis ...
nfequid-o 2211 Bound-variable hypothesis ...
ax46 2212 Proof of a single axiom th...
ax46to4 2213 Re-derivation of ~ ax-4 fr...
ax46to6 2214 Re-derivation of ~ ax-6o f...
ax67 2215 Proof of a single axiom th...
nfa1-o 2216 ` x ` is not free in ` A. ...
ax67to6 2217 Re-derivation of ~ ax-6o f...
ax67to7 2218 Re-derivation of ~ ax-7 fr...
ax467 2219 Proof of a single axiom th...
ax467to4 2220 Re-derivation of ~ ax-4 fr...
ax467to6 2221 Re-derivation of ~ ax-6o f...
ax467to7 2222 Re-derivation of ~ ax-7 fr...
equidqe 2223 ~ equid with existential q...
ax4sp1 2224 A special case of ~ ax-4 w...
equidq 2225 ~ equid with universal qua...
equid1ALT 2226 Identity law for equality ...
ax10from10o 2227 Rederivation of ~ ax-10 fr...
naecoms-o 2228 A commutation rule for dis...
hbnae-o 2229 All variables are effectiv...
dvelimf-o 2230 Proof of ~ dvelimh that us...
dral2-o 2231 Formula-building lemma for...
aev-o 2232 A "distinctor elimination"...
ax17eq 2233 Theorem to add distinct qu...
dveeq2-o 2234 Quantifier introduction wh...
dveeq2-o16 2235 Version of ~ dveeq2 using ...
a16g-o 2236 A generalization of axiom ...
dveeq1-o 2237 Quantifier introduction wh...
dveeq1-o16 2238 Version of ~ dveeq1 using ...
ax17el 2239 Theorem to add distinct qu...
ax10-16 2240 This theorem shows that, g...
dveel2ALT 2241 Version of ~ dveel2 using ...
ax11f 2242 Basis step for constructin...
ax11eq 2243 Basis step for constructin...
ax11el 2244 Basis step for constructin...
ax11indn 2245 Induction step for constru...
ax11indi 2246 Induction step for constru...
ax11indalem 2247 Lemma for ~ ax11inda2 and ...
ax11inda2ALT 2248 A proof of ~ ax11inda2 tha...
ax11inda2 2249 Induction step for constru...
ax11inda 2250 Induction step for constru...
ax11v2-o 2251 Recovery of ~ ax-11o from ...
ax11a2-o 2252 Derive ~ ax-11o from a hyp...
ax10o-o 2253 Show that ~ ax-10o can be ...
eujust 2256 A soundness justification ...
eujustALT 2257 A soundness justification ...
euf 2260 A version of the existenti...
eubid 2261 Formula-building rule for ...
eubidv 2262 Formula-building rule for ...
eubii 2263 Introduce uniqueness quant...
nfeu1 2264 Bound-variable hypothesis ...
nfmo1 2265 Bound-variable hypothesis ...
nfeud2 2266 Bound-variable hypothesis ...
nfmod2 2267 Bound-variable hypothesis ...
nfeud 2268 Deduction version of ~ nfe...
nfmod 2269 Bound-variable hypothesis ...
nfeu 2270 Bound-variable hypothesis ...
nfmo 2271 Bound-variable hypothesis ...
sb8eu 2272 Variable substitution in u...
sb8mo 2273 Variable substitution in u...
cbveu 2274 Rule used to change bound ...
eu1 2275 An alternate way to expres...
mo 2276 Equivalent definitions of ...
euex 2277 Existential uniqueness imp...
eumo0 2278 Existential uniqueness imp...
eu2 2279 An alternate way of defini...
eu3 2280 An alternate way to expres...
euor 2281 Introduce a disjunct into ...
euorv 2282 Introduce a disjunct into ...
mo2 2283 Alternate definition of "a...
sbmo 2284 Substitution into "at most...
mo3 2285 Alternate definition of "a...
mo4f 2286 "At most one" expressed us...
mo4 2287 "At most one" expressed us...
mobid 2288 Formula-building rule for ...
mobidv 2289 Formula-building rule for ...
mobii 2290 Formula-building rule for ...
cbvmo 2291 Rule used to change bound ...
eu5 2292 Uniqueness in terms of "at...
eu4 2293 Uniqueness using implicit ...
eumo 2294 Existential uniqueness imp...
eumoi 2295 "At most one" inferred fro...
exmoeu 2296 Existence in terms of "at ...
exmoeu2 2297 Existence implies "at most...
moabs 2298 Absorption of existence co...
exmo 2299 Something exists or at mos...
moim 2300 "At most one" is preserved...
moimi 2301 "At most one" is preserved...
morimv 2302 Move antecedent outside of...
euimmo 2303 Uniqueness implies "at mos...
euim 2304 Add existential uniqueness...
moan 2305 "At most one" is still the...
moani 2306 "At most one" is still tru...
moor 2307 "At most one" is still the...
mooran1 2308 "At most one" imports disj...
mooran2 2309 "At most one" exports disj...
moanim 2310 Introduction of a conjunct...
euan 2311 Introduction of a conjunct...
moanimv 2312 Introduction of a conjunct...
moaneu 2313 Nested "at most one" and u...
moanmo 2314 Nested "at most one" quant...
euanv 2315 Introduction of a conjunct...
mopick 2316 "At most one" picks a vari...
eupick 2317 Existential uniqueness "pi...
eupicka 2318 Version of ~ eupick with c...
eupickb 2319 Existential uniqueness "pi...
eupickbi 2320 Theorem *14.26 in [Whitehe...
mopick2 2321 "At most one" can show the...
euor2 2322 Introduce or eliminate a d...
moexex 2323 "At most one" double quant...
moexexv 2324 "At most one" double quant...
2moex 2325 Double quantification with...
2euex 2326 Double quantification with...
2eumo 2327 Double quantification with...
2eu2ex 2328 Double existential uniquen...
2moswap 2329 A condition allowing swap ...
2euswap 2330 A condition allowing swap ...
2exeu 2331 Double existential uniquen...
2mo 2332 Two equivalent expressions...
2mos 2333 Double "exists at most one...
2eu1 2334 Double existential uniquen...
2eu2 2335 Double existential uniquen...
2eu3 2336 Double existential uniquen...
2eu4 2337 This theorem provides us w...
2eu5 2338 An alternate definition of...
2eu6 2339 Two equivalent expressions...
2eu7 2340 Two equivalent expressions...
2eu8 2341 Two equivalent expressions...
euequ1 2342 Equality has existential u...
exists1 2343 Two ways to express "only ...
exists2 2344 A condition implying that ...
barbara 2351 "Barbara", one of the fund...
celarent 2352 "Celarent", one of the syl...
darii 2353 "Darii", one of the syllog...
ferio 2354 "Ferio" ("Ferioque"), one ...
barbari 2355 "Barbari", one of the syll...
celaront 2356 "Celaront", one of the syl...
cesare 2357 "Cesare", one of the syllo...
camestres 2358 "Camestres", one of the sy...
festino 2359 "Festino", one of the syll...
baroco 2360 "Baroco", one of the syllo...
cesaro 2361 "Cesaro", one of the syllo...
camestros 2362 "Camestros", one of the sy...
datisi 2363 "Datisi", one of the syllo...
disamis 2364 "Disamis", one of the syll...
ferison 2365 "Ferison", one of the syll...
bocardo 2366 "Bocardo", one of the syll...
felapton 2367 "Felapton", one of the syl...
darapti 2368 "Darapti", one of the syll...
calemes 2369 "Calemes", one of the syll...
dimatis 2370 "Dimatis", one of the syll...
fresison 2371 "Fresison", one of the syl...
calemos 2372 "Calemos", one of the syll...
fesapo 2373 "Fesapo", one of the syllo...
bamalip 2374 "Bamalip", one of the syll...
axi4 2375 Specialization (intuitioni...
axi5r 2376 Converse of ax-5o (intuiti...
axial 2377 ` x ` is not free in ` A. ...
axie1 2378 ` x ` is bound in ` E. x p...
axie2 2379 A key property of existent...
axi9 2380 Axiom of existence (intuit...
axi10 2381 Axiom of Quantifier Substi...
axi11e 2382 Axiom of Variable Substitu...
axi12 2383 Axiom of Quantifier Introd...
axbnd 2384 Axiom of Bundling (intuiti...
axext2 2386 The Axiom of Extensionalit...
axext3 2387 A generalization of the Ax...
axext4 2388 A bidirectional version of...
bm1.1 2389 Any set defined by a prope...
abid 2392 Simplification of class ab...
hbab1 2393 Bound-variable hypothesis ...
nfsab1 2394 Bound-variable hypothesis ...
hbab 2395 Bound-variable hypothesis ...
nfsab 2396 Bound-variable hypothesis ...
dfcleq 2398 The same as ~ df-cleq with...
cvjust 2399 Every set is a class. Pro...
eqriv 2401 Infer equality of classes ...
eqrdv 2402 Deduce equality of classes...
eqrdav 2403 Deduce equality of classes...
eqid 2404 Law of identity (reflexivi...
eqidd 2405 Class identity law with an...
eqcom 2406 Commutative law for class ...
eqcoms 2407 Inference applying commuta...
eqcomi 2408 Inference from commutative...
eqcomd 2409 Deduction from commutative...
eqeq1 2410 Equality implies equivalen...
eqeq1i 2411 Inference from equality to...
eqeq1d 2412 Deduction from equality to...
eqeq2 2413 Equality implies equivalen...
eqeq2i 2414 Inference from equality to...
eqeq2d 2415 Deduction from equality to...
eqeq12 2416 Equality relationship amon...
eqeq12i 2417 A useful inference for sub...
eqeq12d 2418 A useful inference for sub...
eqeqan12d 2419 A useful inference for sub...
eqeqan12rd 2420 A useful inference for sub...
eqtr 2421 Transitive law for class e...
eqtr2 2422 A transitive law for class...
eqtr3 2423 A transitive law for class...
eqtri 2424 An equality transitivity i...
eqtr2i 2425 An equality transitivity i...
eqtr3i 2426 An equality transitivity i...
eqtr4i 2427 An equality transitivity i...
3eqtri 2428 An inference from three ch...
3eqtrri 2429 An inference from three ch...
3eqtr2i 2430 An inference from three ch...
3eqtr2ri 2431 An inference from three ch...
3eqtr3i 2432 An inference from three ch...
3eqtr3ri 2433 An inference from three ch...
3eqtr4i 2434 An inference from three ch...
3eqtr4ri 2435 An inference from three ch...
eqtrd 2436 An equality transitivity d...
eqtr2d 2437 An equality transitivity d...
eqtr3d 2438 An equality transitivity e...
eqtr4d 2439 An equality transitivity e...
3eqtrd 2440 A deduction from three cha...
3eqtrrd 2441 A deduction from three cha...
3eqtr2d 2442 A deduction from three cha...
3eqtr2rd 2443 A deduction from three cha...
3eqtr3d 2444 A deduction from three cha...
3eqtr3rd 2445 A deduction from three cha...
3eqtr4d 2446 A deduction from three cha...
3eqtr4rd 2447 A deduction from three cha...
syl5eq 2448 An equality transitivity d...
syl5req 2449 An equality transitivity d...
syl5eqr 2450 An equality transitivity d...
syl5reqr 2451 An equality transitivity d...
syl6eq 2452 An equality transitivity d...
syl6req 2453 An equality transitivity d...
syl6eqr 2454 An equality transitivity d...
syl6reqr 2455 An equality transitivity d...
sylan9eq 2456 An equality transitivity d...
sylan9req 2457 An equality transitivity d...
sylan9eqr 2458 An equality transitivity d...
3eqtr3g 2459 A chained equality inferen...
3eqtr3a 2460 A chained equality inferen...
3eqtr4g 2461 A chained equality inferen...
3eqtr4a 2462 A chained equality inferen...
eq2tri 2463 A compound transitive infe...
eleq1 2464 Equality implies equivalen...
eleq2 2465 Equality implies equivalen...
eleq12 2466 Equality implies equivalen...
eleq1i 2467 Inference from equality to...
eleq2i 2468 Inference from equality to...
eleq12i 2469 Inference from equality to...
eleq1d 2470 Deduction from equality to...
eleq2d 2471 Deduction from equality to...
eleq12d 2472 Deduction from equality to...
eleq1a 2473 A transitive-type law rela...
eqeltri 2474 Substitution of equal clas...
eqeltrri 2475 Substitution of equal clas...
eleqtri 2476 Substitution of equal clas...
eleqtrri 2477 Substitution of equal clas...
eqeltrd 2478 Substitution of equal clas...
eqeltrrd 2479 Deduction that substitutes...
eleqtrd 2480 Deduction that substitutes...
eleqtrrd 2481 Deduction that substitutes...
3eltr3i 2482 Substitution of equal clas...
3eltr4i 2483 Substitution of equal clas...
3eltr3d 2484 Substitution of equal clas...
3eltr4d 2485 Substitution of equal clas...
3eltr3g 2486 Substitution of equal clas...
3eltr4g 2487 Substitution of equal clas...
syl5eqel 2488 B membership and equality ...
syl5eqelr 2489 B membership and equality ...
syl5eleq 2490 B membership and equality ...
syl5eleqr 2491 B membership and equality ...
syl6eqel 2492 A membership and equality ...
syl6eqelr 2493 A membership and equality ...
syl6eleq 2494 A membership and equality ...
syl6eleqr 2495 A membership and equality ...
eleq2s 2496 Substitution of equal clas...
eqneltrd 2497 If a class is not an eleme...
eqneltrrd 2498 If a class is not an eleme...
neleqtrd 2499 If a class is not an eleme...
neleqtrrd 2500 If a class is not an eleme...
cleqh 2501 Establish equality between...
nelneq 2502 A way of showing two class...
nelneq2 2503 A way of showing two class...
eqsb3lem 2504 Lemma for ~ eqsb3 . (Cont...
eqsb3 2505 Substitution applied to an...
clelsb3 2506 Substitution applied to an...
hbxfreq 2507 A utility lemma to transfe...
hblem 2508 Change the free variable o...
abeq2 2509 Equality of a class variab...
abeq1 2510 Equality of a class variab...
abeq2i 2511 Equality of a class variab...
abeq1i 2512 Equality of a class variab...
abeq2d 2513 Equality of a class variab...
abbi 2514 Equivalent wff's correspon...
abbi2i 2515 Equality of a class variab...
abbii 2516 Equivalent wff's yield equ...
abbid 2517 Equivalent wff's yield equ...
abbidv 2518 Equivalent wff's yield equ...
abbi2dv 2519 Deduction from a wff to a ...
abbi1dv 2520 Deduction from a wff to a ...
abid2 2521 A simplification of class ...
cbvab 2522 Rule used to change bound ...
cbvabv 2523 Rule used to change bound ...
clelab 2524 Membership of a class vari...
clabel 2525 Membership of a class abst...
sbab 2526 The right-hand side of the...
nfcjust 2528 Justification theorem for ...
nfci 2530 Deduce that a class ` A ` ...
nfcii 2531 Deduce that a class ` A ` ...
nfcr 2532 Consequence of the not-fre...
nfcrii 2533 Consequence of the not-fre...
nfcri 2534 Consequence of the not-fre...
nfcd 2535 Deduce that a class ` A ` ...
nfceqi 2536 Equality theorem for class...
nfcxfr 2537 A utility lemma to transfe...
nfcxfrd 2538 A utility lemma to transfe...
nfceqdf 2539 An equality theorem for ef...
nfcv 2540 If ` x ` is disjoint from ...
nfcvd 2541 If ` x ` is disjoint from ...
nfab1 2542 Bound-variable hypothesis ...
nfnfc1 2543 ` x ` is bound in ` F/_ x ...
nfab 2544 Bound-variable hypothesis ...
nfaba1 2545 Bound-variable hypothesis ...
nfnfc 2546 Hypothesis builder for ` F...
nfeq 2547 Hypothesis builder for equ...
nfel 2548 Hypothesis builder for ele...
nfeq1 2549 Hypothesis builder for equ...
nfel1 2550 Hypothesis builder for ele...
nfeq2 2551 Hypothesis builder for equ...
nfel2 2552 Hypothesis builder for ele...
nfcrd 2553 Consequence of the not-fre...
nfeqd 2554 Hypothesis builder for equ...
nfeld 2555 Hypothesis builder for ele...
drnfc1 2556 Formula-building lemma for...
drnfc2 2557 Formula-building lemma for...
nfabd2 2558 Bound-variable hypothesis ...
nfabd 2559 Bound-variable hypothesis ...
dvelimdc 2560 Deduction form of ~ dvelim...
dvelimc 2561 Version of ~ dvelim for cl...
nfcvf 2562 If ` x ` and ` y ` are dis...
nfcvf2 2563 If ` x ` and ` y ` are dis...
cleqf 2564 Establish equality between...
abid2f 2565 A simplification of class ...
sbabel 2566 Theorem to move a substitu...
nne 2571 Negation of inequality. (...
neirr 2572 No class is unequal to its...
exmidne 2573 Excluded middle with equal...
nonconne 2574 Law of noncontradiction wi...
neeq1 2575 Equality theorem for inequ...
neeq2 2576 Equality theorem for inequ...
neeq1i 2577 Inference for inequality. ...
neeq2i 2578 Inference for inequality. ...
neeq12i 2579 Inference for inequality. ...
neeq1d 2580 Deduction for inequality. ...
neeq2d 2581 Deduction for inequality. ...
neeq12d 2582 Deduction for inequality. ...
neneqd 2583 Deduction eliminating ineq...
eqnetri 2584 Substitution of equal clas...
eqnetrd 2585 Substitution of equal clas...
eqnetrri 2586 Substitution of equal clas...
eqnetrrd 2587 Substitution of equal clas...
neeqtri 2588 Substitution of equal clas...
neeqtrd 2589 Substitution of equal clas...
neeqtrri 2590 Substitution of equal clas...
neeqtrrd 2591 Substitution of equal clas...
syl5eqner 2592 B chained equality inferen...
3netr3d 2593 Substitution of equality i...
3netr4d 2594 Substitution of equality i...
3netr3g 2595 Substitution of equality i...
3netr4g 2596 Substitution of equality i...
necon3abii 2597 Deduction from equality to...
necon3bbii 2598 Deduction from equality to...
necon3bii 2599 Inference from equality to...
necon3abid 2600 Deduction from equality to...
necon3bbid 2601 Deduction from equality to...
necon3bid 2602 Deduction from equality to...
necon3ad 2603 Contrapositive law deducti...
necon3bd 2604 Contrapositive law deducti...
necon3d 2605 Contrapositive law deducti...
necon3i 2606 Contrapositive inference f...
necon3ai 2607 Contrapositive inference f...
necon3bi 2608 Contrapositive inference f...
necon1ai 2609 Contrapositive inference f...
necon1bi 2610 Contrapositive inference f...
necon1i 2611 Contrapositive inference f...
necon2ai 2612 Contrapositive inference f...
necon2bi 2613 Contrapositive inference f...
necon2i 2614 Contrapositive inference f...
necon2ad 2615 Contrapositive inference f...
necon2bd 2616 Contrapositive inference f...
necon2d 2617 Contrapositive inference f...
necon1abii 2618 Contrapositive inference f...
necon1bbii 2619 Contrapositive inference f...
necon1abid 2620 Contrapositive deduction f...
necon1bbid 2621 Contrapositive inference f...
necon2abii 2622 Contrapositive inference f...
necon2bbii 2623 Contrapositive inference f...
necon2abid 2624 Contrapositive deduction f...
necon2bbid 2625 Contrapositive deduction f...
necon4ai 2626 Contrapositive inference f...
necon4i 2627 Contrapositive inference f...
necon4ad 2628 Contrapositive inference f...
necon4bd 2629 Contrapositive inference f...
necon4d 2630 Contrapositive inference f...
necon4abid 2631 Contrapositive law deducti...
necon4bbid 2632 Contrapositive law deducti...
necon4bid 2633 Contrapositive law deducti...
necon1ad 2634 Contrapositive deduction f...
necon1bd 2635 Contrapositive deduction f...
necon1d 2636 Contrapositive law deducti...
neneqad 2637 If it is not the case that...
nebi 2638 Contraposition law for ine...
pm13.18 2639 Theorem *13.18 in [Whitehe...
pm13.181 2640 Theorem *13.181 in [Whiteh...
pm2.21ddne 2641 A contradiction implies an...
pm2.61ne 2642 Deduction eliminating an i...
pm2.61ine 2643 Inference eliminating an i...
pm2.61dne 2644 Deduction eliminating an i...
pm2.61dane 2645 Deduction eliminating an i...
pm2.61da2ne 2646 Deduction eliminating two ...
pm2.61da3ne 2647 Deduction eliminating thre...
necom 2648 Commutation of inequality....
necomi 2649 Inference from commutative...
necomd 2650 Deduction from commutative...
neor 2651 Logical OR with an equalit...
neanior 2652 A De Morgan's law for ineq...
ne3anior 2653 A De Morgan's law for ineq...
neorian 2654 A De Morgan's law for ineq...
nemtbir 2655 An inference from an inequ...
nelne1 2656 Two classes are different ...
nelne2 2657 Two classes are different ...
nfne 2658 Bound-variable hypothesis ...
nfned 2659 Bound-variable hypothesis ...
neleq1 2660 Equality theorem for negat...
neleq2 2661 Equality theorem for negat...
neleq12d 2662 Equality theorem for negat...
nfnel 2663 Bound-variable hypothesis ...
nfneld 2664 Bound-variable hypothesis ...
nnel 2665 Negation of negated member...
ralnex 2676 Relationship between restr...
rexnal 2677 Relationship between restr...
dfral2 2678 Relationship between restr...
dfrex2 2679 Relationship between restr...
ralbida 2680 Formula-building rule for ...
rexbida 2681 Formula-building rule for ...
ralbidva 2682 Formula-building rule for ...
rexbidva 2683 Formula-building rule for ...
ralbid 2684 Formula-building rule for ...
rexbid 2685 Formula-building rule for ...
ralbidv 2686 Formula-building rule for ...
rexbidv 2687 Formula-building rule for ...
ralbidv2 2688 Formula-building rule for ...
rexbidv2 2689 Formula-building rule for ...
ralbii 2690 Inference adding restricte...
rexbii 2691 Inference adding restricte...
2ralbii 2692 Inference adding two restr...
2rexbii 2693 Inference adding two restr...
ralbii2 2694 Inference adding different...
rexbii2 2695 Inference adding different...
raleqbii 2696 Equality deduction for res...
rexeqbii 2697 Equality deduction for res...
ralbiia 2698 Inference adding restricte...
rexbiia 2699 Inference adding restricte...
2rexbiia 2700 Inference adding two restr...
r2alf 2701 Double restricted universa...
r2exf 2702 Double restricted existent...
r2al 2703 Double restricted universa...
r2ex 2704 Double restricted existent...
2ralbida 2705 Formula-building rule for ...
2ralbidva 2706 Formula-building rule for ...
2rexbidva 2707 Formula-building rule for ...
2ralbidv 2708 Formula-building rule for ...
2rexbidv 2709 Formula-building rule for ...
rexralbidv 2710 Formula-building rule for ...
ralinexa 2711 A transformation of restri...
rexanali 2712 A transformation of restri...
risset 2713 Two ways to say " ` A ` be...
hbral 2714 Bound-variable hypothesis ...
hbra1 2715 ` x ` is not free in ` A. ...
nfra1 2716 ` x ` is not free in ` A. ...
nfrald 2717 Deduction version of ~ nfr...
nfrexd 2718 Deduction version of ~ nfr...
nfral 2719 Bound-variable hypothesis ...
nfra2 2720 Similar to Lemma 24 of [Mo...
nfrex 2721 Bound-variable hypothesis ...
nfre1 2722 ` x ` is not free in ` E. ...
r3al 2723 Triple restricted universa...
alral 2724 Universal quantification i...
rexex 2725 Restricted existence impli...
rsp 2726 Restricted specialization....
rspe 2727 Restricted specialization....
rsp2 2728 Restricted specialization....
rsp2e 2729 Restricted specialization....
rspec 2730 Specialization rule for re...
rgen 2731 Generalization rule for re...
rgen2a 2732 Generalization rule for re...
rgenw 2733 Generalization rule for re...
rgen2w 2734 Generalization rule for re...
mprg 2735 Modus ponens combined with...
mprgbir 2736 Modus ponens on biconditio...
ralim 2737 Distribution of restricted...
ralimi2 2738 Inference quantifying both...
ralimia 2739 Inference quantifying both...
ralimiaa 2740 Inference quantifying both...
ralimi 2741 Inference quantifying both...
ral2imi 2742 Inference quantifying ante...
ralimdaa 2743 Deduction quantifying both...
ralimdva 2744 Deduction quantifying both...
ralimdv 2745 Deduction quantifying both...
ralimdv2 2746 Inference quantifying both...
ralrimi 2747 Inference from Theorem 19....
ralrimiv 2748 Inference from Theorem 19....
ralrimiva 2749 Inference from Theorem 19....
ralrimivw 2750 Inference from Theorem 19....
r19.21t 2751 Theorem 19.21 of [Margaris...
r19.21 2752 Theorem 19.21 of [Margaris...
r19.21v 2753 Theorem 19.21 of [Margaris...
ralrimd 2754 Inference from Theorem 19....
ralrimdv 2755 Inference from Theorem 19....
ralrimdva 2756 Inference from Theorem 19....
ralrimivv 2757 Inference from Theorem 19....
ralrimivva 2758 Inference from Theorem 19....
ralrimivvva 2759 Inference from Theorem 19....
ralrimdvv 2760 Inference from Theorem 19....
ralrimdvva 2761 Inference from Theorem 19....
rgen2 2762 Generalization rule for re...
rgen3 2763 Generalization rule for re...
r19.21bi 2764 Inference from Theorem 19....
rspec2 2765 Specialization rule for re...
rspec3 2766 Specialization rule for re...
r19.21be 2767 Inference from Theorem 19....
nrex 2768 Inference adding restricte...
nrexdv 2769 Deduction adding restricte...
rexim 2770 Theorem 19.22 of [Margaris...
reximia 2771 Inference quantifying both...
reximi2 2772 Inference quantifying both...
reximi 2773 Inference quantifying both...
reximdai 2774 Deduction from Theorem 19....
reximdv2 2775 Deduction quantifying both...
reximdvai 2776 Deduction quantifying both...
reximdv 2777 Deduction from Theorem 19....
reximdva 2778 Deduction quantifying both...
r19.12 2779 Theorem 19.12 of [Margaris...
r19.23t 2780 Closed theorem form of ~ r...
r19.23 2781 Theorem 19.23 of [Margaris...
r19.23v 2782 Theorem 19.23 of [Margaris...
rexlimi 2783 Inference from Theorem 19....
rexlimiv 2784 Inference from Theorem 19....
rexlimiva 2785 Inference from Theorem 19....
rexlimivw 2786 Weaker version of ~ rexlim...
rexlimd 2787 Deduction from Theorem 19....
rexlimd2 2788 Version of ~ rexlimd with ...
rexlimdv 2789 Inference from Theorem 19....
rexlimdva 2790 Inference from Theorem 19....
rexlimdvaa 2791 Inference from Theorem 19....
rexlimdv3a 2792 Inference from Theorem 19....
rexlimdvw 2793 Inference from Theorem 19....
rexlimddv 2794 Restricted existential eli...
rexlimivv 2795 Inference from Theorem 19....
rexlimdvv 2796 Inference from Theorem 19....
rexlimdvva 2797 Inference from Theorem 19....
r19.26 2798 Theorem 19.26 of [Margaris...
r19.26-2 2799 Theorem 19.26 of [Margaris...
r19.26-3 2800 Theorem 19.26 of [Margaris...
r19.26m 2801 Theorem 19.26 of [Margaris...
ralbi 2802 Distribute a restricted un...
ralbiim 2803 Split a biconditional and ...
r19.27av 2804 Restricted version of one ...
r19.28av 2805 Restricted version of one ...
r19.29 2806 Theorem 19.29 of [Margaris...
r19.29r 2807 Variation of Theorem 19.29...
r19.29af2 2808 A commonly used pattern ba...
r19.29af 2809 A commonly used pattern ba...
r19.29a 2810 A commonly used pattern ba...
r19.29d2r 2811 Theorem 19.29 of [Margaris...
r19.29_2a 2812 A commonly used pattern ba...
r19.30 2813 Theorem 19.30 of [Margaris...
r19.32v 2814 Theorem 19.32 of [Margaris...
r19.35 2815 Restricted quantifier vers...
r19.36av 2816 One direction of a restric...
r19.37 2817 Restricted version of one ...
r19.37av 2818 Restricted version of one ...
r19.40 2819 Restricted quantifier vers...
r19.41 2820 Restricted quantifier vers...
r19.41v 2821 Restricted quantifier vers...
r19.42v 2822 Restricted version of Theo...
r19.43 2823 Restricted version of Theo...
r19.44av 2824 One direction of a restric...
r19.45av 2825 Restricted version of one ...
ralcomf 2826 Commutation of restricted ...
rexcomf 2827 Commutation of restricted ...
ralcom 2828 Commutation of restricted ...
rexcom 2829 Commutation of restricted ...
rexcom13 2830 Swap 1st and 3rd restricte...
rexrot4 2831 Rotate existential restric...
ralcom2 2832 Commutation of restricted ...
ralcom3 2833 A commutative law for rest...
reean 2834 Rearrange existential quan...
reeanv 2835 Rearrange existential quan...
3reeanv 2836 Rearrange three existentia...
2ralor 2837 Distribute quantification ...
nfreu1 2838 ` x ` is not free in ` E! ...
nfrmo1 2839 ` x ` is not free in ` E* ...
nfreud 2840 Deduction version of ~ nfr...
nfrmod 2841 Deduction version of ~ nfr...
nfreu 2842 Bound-variable hypothesis ...
nfrmo 2843 Bound-variable hypothesis ...
rabid 2844 An "identity" law of concr...
rabid2 2845 An "identity" law for rest...
rabbi 2846 Equivalent wff's correspon...
rabswap 2847 Swap with a membership rel...
nfrab1 2848 The abstraction variable i...
nfrab 2849 A variable not free in a w...
reubida 2850 Formula-building rule for ...
reubidva 2851 Formula-building rule for ...
reubidv 2852 Formula-building rule for ...
reubiia 2853 Formula-building rule for ...
reubii 2854 Formula-building rule for ...
rmobida 2855 Formula-building rule for ...
rmobidva 2856 Formula-building rule for ...
rmobidv 2857 Formula-building rule for ...
rmobiia 2858 Formula-building rule for ...
rmobii 2859 Formula-building rule for ...
raleqf 2860 Equality theorem for restr...
rexeqf 2861 Equality theorem for restr...
reueq1f 2862 Equality theorem for restr...
rmoeq1f 2863 Equality theorem for restr...
raleq 2864 Equality theorem for restr...
rexeq 2865 Equality theorem for restr...
reueq1 2866 Equality theorem for restr...
rmoeq1 2867 Equality theorem for restr...
raleqi 2868 Equality inference for res...
rexeqi 2869 Equality inference for res...
raleqdv 2870 Equality deduction for res...
rexeqdv 2871 Equality deduction for res...
raleqbi1dv 2872 Equality deduction for res...
rexeqbi1dv 2873 Equality deduction for res...
reueqd 2874 Equality deduction for res...
rmoeqd 2875 Equality deduction for res...
raleqbidv 2876 Equality deduction for res...
rexeqbidv 2877 Equality deduction for res...
raleqbidva 2878 Equality deduction for res...
rexeqbidva 2879 Equality deduction for res...
mormo 2880 Unrestricted "at most one"...
reu5 2881 Restricted uniqueness in t...
reurex 2882 Restricted unique existenc...
reurmo 2883 Restricted existential uni...
rmo5 2884 Restricted "at most one" i...
nrexrmo 2885 Nonexistence implies restr...
cbvralf 2886 Rule used to change bound ...
cbvrexf 2887 Rule used to change bound ...
cbvral 2888 Rule used to change bound ...
cbvrex 2889 Rule used to change bound ...
cbvreu 2890 Change the bound variable ...
cbvrmo 2891 Change the bound variable ...
cbvralv 2892 Change the bound variable ...
cbvrexv 2893 Change the bound variable ...
cbvreuv 2894 Change the bound variable ...
cbvrmov 2895 Change the bound variable ...
cbvraldva2 2896 Rule used to change the bo...
cbvrexdva2 2897 Rule used to change the bo...
cbvraldva 2898 Rule used to change the bo...
cbvrexdva 2899 Rule used to change the bo...
cbvral2v 2900 Change bound variables of ...
cbvrex2v 2901 Change bound variables of ...
cbvral3v 2902 Change bound variables of ...
cbvralsv 2903 Change bound variable by u...
cbvrexsv 2904 Change bound variable by u...
sbralie 2905 Implicit to explicit subst...
rabbiia 2906 Equivalent wff's yield equ...
rabbidva 2907 Equivalent wff's yield equ...
rabbidv 2908 Equivalent wff's yield equ...
rabeqf 2909 Equality theorem for restr...
rabeq 2910 Equality theorem for restr...
rabeqbidv 2911 Equality of restricted cla...
rabeqbidva 2912 Equality of restricted cla...
rabeq2i 2913 Inference rule from equali...
cbvrab 2914 Rule to change the bound v...
cbvrabv 2915 Rule to change the bound v...
vjust 2917 Soundness justification th...
vex 2919 All set variables are sets...
isset 2920 Two ways to say " ` A ` is...
issetf 2921 A version of isset that do...
isseti 2922 A way to say " ` A ` is a ...
issetri 2923 A way to say " ` A ` is a ...
elex 2924 If a class is a member of ...
elexi 2925 If a class is a member of ...
elisset 2926 An element of a class exis...
elex22 2927 If two classes each contai...
elex2 2928 If a class contains anothe...
ralv 2929 A universal quantifier res...
rexv 2930 An existential quantifier ...
reuv 2931 A uniqueness quantifier re...
rmov 2932 A uniqueness quantifier re...
rabab 2933 A class abstraction restri...
ralcom4 2934 Commutation of restricted ...
rexcom4 2935 Commutation of restricted ...
rexcom4a 2936 Specialized existential co...
rexcom4b 2937 Specialized existential co...
ceqsalt 2938 Closed theorem version of ...
ceqsralt 2939 Restricted quantifier vers...
ceqsalg 2940 A representation of explic...
ceqsal 2941 A representation of explic...
ceqsalv 2942 A representation of explic...
ceqsralv 2943 Restricted quantifier vers...
gencl 2944 Implicit substitution for ...
2gencl 2945 Implicit substitution for ...
3gencl 2946 Implicit substitution for ...
cgsexg 2947 Implicit substitution infe...
cgsex2g 2948 Implicit substitution infe...
cgsex4g 2949 An implicit substitution i...
ceqsex 2950 Elimination of an existent...
ceqsexv 2951 Elimination of an existent...
ceqsex2 2952 Elimination of two existen...
ceqsex2v 2953 Elimination of two existen...
ceqsex3v 2954 Elimination of three exist...
ceqsex4v 2955 Elimination of four existe...
ceqsex6v 2956 Elimination of six existen...
ceqsex8v 2957 Elimination of eight exist...
gencbvex 2958 Change of bound variable u...
gencbvex2 2959 Restatement of ~ gencbvex ...
gencbval 2960 Change of bound variable u...
sbhypf 2961 Introduce an explicit subs...
vtoclgft 2962 Closed theorem form of ~ v...
vtocldf 2963 Implicit substitution of a...
vtocld 2964 Implicit substitution of a...
vtoclf 2965 Implicit substitution of a...
vtocl 2966 Implicit substitution of a...
vtocl2 2967 Implicit substitution of c...
vtocl3 2968 Implicit substitution of c...
vtoclb 2969 Implicit substitution of a...
vtoclgf 2970 Implicit substitution of a...
vtoclg 2971 Implicit substitution of a...
vtoclbg 2972 Implicit substitution of a...
vtocl2gf 2973 Implicit substitution of a...
vtocl3gf 2974 Implicit substitution of a...
vtocl2g 2975 Implicit substitution of 2...
vtoclgaf 2976 Implicit substitution of a...
vtoclga 2977 Implicit substitution of a...
vtocl2gaf 2978 Implicit substitution of 2...
vtocl2ga 2979 Implicit substitution of 2...
vtocl3gaf 2980 Implicit substitution of 3...
vtocl3ga 2981 Implicit substitution of 3...
vtocleg 2982 Implicit substitution of a...
vtoclegft 2983 Implicit substitution of a...
vtoclef 2984 Implicit substitution of a...
vtocle 2985 Implicit substitution of a...
vtoclri 2986 Implicit substitution of a...
spcimgft 2987 A closed version of ~ spci...
spcgft 2988 A closed version of ~ spcg...
spcimgf 2989 Rule of specialization, us...
spcimegf 2990 Existential specialization...
spcgf 2991 Rule of specialization, us...
spcegf 2992 Existential specialization...
spcimdv 2993 Restricted specialization,...
spcdv 2994 Rule of specialization, us...
spcimedv 2995 Restricted existential spe...
spcgv 2996 Rule of specialization, us...
spcegv 2997 Existential specialization...
spc2egv 2998 Existential specialization...
spc2gv 2999 Specialization with 2 quan...
spc3egv 3000 Existential specialization...
spc3gv 3001 Specialization with 3 quan...
spcv 3002 Rule of specialization, us...
spcev 3003 Existential specialization...
spc2ev 3004 Existential specialization...
rspct 3005 A closed version of ~ rspc...
rspc 3006 Restricted specialization,...
rspce 3007 Restricted existential spe...
rspcv 3008 Restricted specialization,...
rspccv 3009 Restricted specialization,...
rspcva 3010 Restricted specialization,...
rspccva 3011 Restricted specialization,...
rspcev 3012 Restricted existential spe...
rspcimdv 3013 Restricted specialization,...
rspcimedv 3014 Restricted existential spe...
rspcdv 3015 Restricted specialization,...
rspcedv 3016 Restricted existential spe...
rspc2 3017 2-variable restricted spec...
rspc2v 3018 2-variable restricted spec...
rspc2va 3019 2-variable restricted spec...
rspc2ev 3020 2-variable restricted exis...
rspc3v 3021 3-variable restricted spec...
rspc3ev 3022 3-variable restricted exis...
eqvinc 3023 A variable introduction la...
eqvincf 3024 A variable introduction la...
alexeq 3025 Two ways to express substi...
ceqex 3026 Equality implies equivalen...
ceqsexg 3027 A representation of explic...
ceqsexgv 3028 Elimination of an existent...
ceqsrexv 3029 Elimination of a restricte...
ceqsrexbv 3030 Elimination of a restricte...
ceqsrex2v 3031 Elimination of a restricte...
clel2 3032 An alternate definition of...
clel3g 3033 An alternate definition of...
clel3 3034 An alternate definition of...
clel4 3035 An alternate definition of...
pm13.183 3036 Compare theorem *13.183 in...
rr19.3v 3037 Restricted quantifier vers...
rr19.28v 3038 Restricted quantifier vers...
elabgt 3039 Membership in a class abst...
elabgf 3040 Membership in a class abst...
elabf 3041 Membership in a class abst...
elab 3042 Membership in a class abst...
elabg 3043 Membership in a class abst...
elab2g 3044 Membership in a class abst...
elab2 3045 Membership in a class abst...
elab4g 3046 Membership in a class abst...
elab3gf 3047 Membership in a class abst...
elab3g 3048 Membership in a class abst...
elab3 3049 Membership in a class abst...
elrabi 3050 Implication for the member...
elrabf 3051 Membership in a restricted...
elrab 3052 Membership in a restricted...
elrab3 3053 Membership in a restricted...
elrab2 3054 Membership in a class abst...
ralab 3055 Universal quantification o...
ralrab 3056 Universal quantification o...
rexab 3057 Existential quantification...
rexrab 3058 Existential quantification...
ralab2 3059 Universal quantification o...
ralrab2 3060 Universal quantification o...
rexab2 3061 Existential quantification...
rexrab2 3062 Existential quantification...
abidnf 3063 Identity used to create cl...
dedhb 3064 A deduction theorem for co...
eqeu 3065 A condition which implies ...
eueq 3066 Equality has existential u...
eueq1 3067 Equality has existential u...
eueq2 3068 Equality has existential u...
eueq3 3069 Equality has existential u...
moeq 3070 There is at most one set e...
moeq3 3071 "At most one" property of ...
mosub 3072 "At most one" remains true...
mo2icl 3073 Theorem for inferring "at ...
mob2 3074 Consequence of "at most on...
moi2 3075 Consequence of "at most on...
mob 3076 Equality implied by "at mo...
moi 3077 Equality implied by "at mo...
morex 3078 Derive membership from uni...
euxfr2 3079 Transfer existential uniqu...
euxfr 3080 Transfer existential uniqu...
euind 3081 Existential uniqueness via...
reu2 3082 A way to express restricte...
reu6 3083 A way to express restricte...
reu3 3084 A way to express restricte...
reu6i 3085 A condition which implies ...
eqreu 3086 A condition which implies ...
rmo4 3087 Restricted "at most one" u...
reu4 3088 Restricted uniqueness usin...
reu7 3089 Restricted uniqueness usin...
reu8 3090 Restricted uniqueness usin...
reueq 3091 Equality has existential u...
rmoan 3092 Restricted "at most one" s...
rmoim 3093 Restricted "at most one" i...
rmoimia 3094 Restricted "at most one" i...
rmoimi2 3095 Restricted "at most one" i...
2reuswap 3096 A condition allowing swap ...
reuind 3097 Existential uniqueness via...
2rmorex 3098 Double restricted quantifi...
2reu5lem1 3099 Lemma for ~ 2reu5 . Note ...
2reu5lem2 3100 Lemma for ~ 2reu5 . (Cont...
2reu5lem3 3101 Lemma for ~ 2reu5 . This ...
2reu5 3102 Double restricted existent...
nelrdva 3103 Deduce negative membership...
cdeqi 3106 Deduce conditional equalit...
cdeqri 3107 Property of conditional eq...
cdeqth 3108 Deduce conditional equalit...
cdeqnot 3109 Distribute conditional equ...
cdeqal 3110 Distribute conditional equ...
cdeqab 3111 Distribute conditional equ...
cdeqal1 3112 Distribute conditional equ...
cdeqab1 3113 Distribute conditional equ...
cdeqim 3114 Distribute conditional equ...
cdeqcv 3115 Conditional equality for s...
cdeqeq 3116 Distribute conditional equ...
cdeqel 3117 Distribute conditional equ...
nfcdeq 3118 If we have a conditional e...
nfccdeq 3119 Variation of ~ nfcdeq for ...
ru 3120 Russell's Paradox. Propos...
dfsbcq 3123 This theorem, which is sim...
dfsbcq2 3124 This theorem, which is sim...
sbsbc 3125 Show that ~ df-sb and ~ df...
sbceq1d 3126 Equality theorem for class...
sbceq1dd 3127 Equality theorem for class...
sbc8g 3128 This is the closest we can...
sbc2or 3129 The disjunction of two equ...
sbcex 3130 By our definition of prope...
sbceq1a 3131 Equality theorem for class...
sbceq2a 3132 Equality theorem for class...
spsbc 3133 Specialization: if a formu...
spsbcd 3134 Specialization: if a formu...
sbcth 3135 A substitution into a theo...
sbcthdv 3136 Deduction version of ~ sbc...
sbcid 3137 An identity theorem for su...
nfsbc1d 3138 Deduction version of ~ nfs...
nfsbc1 3139 Bound-variable hypothesis ...
nfsbc1v 3140 Bound-variable hypothesis ...
nfsbcd 3141 Deduction version of ~ nfs...
nfsbc 3142 Bound-variable hypothesis ...
sbcco 3143 A composition law for clas...
sbcco2 3144 A composition law for clas...
sbc5 3145 An equivalence for class s...
sbc6g 3146 An equivalence for class s...
sbc6 3147 An equivalence for class s...
sbc7 3148 An equivalence for class s...
cbvsbc 3149 Change bound variables in ...
cbvsbcv 3150 Change the bound variable ...
sbciegft 3151 Conversion of implicit sub...
sbciegf 3152 Conversion of implicit sub...
sbcieg 3153 Conversion of implicit sub...
sbcie2g 3154 Conversion of implicit sub...
sbcie 3155 Conversion of implicit sub...
sbciedf 3156 Conversion of implicit sub...
sbcied 3157 Conversion of implicit sub...
sbcied2 3158 Conversion of implicit sub...
elrabsf 3159 Membership in a restricted...
eqsbc3 3160 Substitution applied to an...
sbcng 3161 Move negation in and out o...
sbcimg 3162 Distribution of class subs...
sbcan 3163 Distribution of class subs...
sbcang 3164 Distribution of class subs...
sbcor 3165 Distribution of class subs...
sbcorg 3166 Distribution of class subs...
sbcbig 3167 Distribution of class subs...
sbcal 3168 Move universal quantifier ...
sbcalg 3169 Move universal quantifier ...
sbcex2 3170 Move existential quantifie...
sbcexg 3171 Move existential quantifie...
sbceqal 3172 Set theory version of ~ sb...
sbeqalb 3173 Theorem *14.121 in [Whiteh...
sbcbid 3174 Formula-building deduction...
sbcbidv 3175 Formula-building deduction...
sbcbii 3176 Formula-building inference...
sbcbiiOLD 3177 Formula-building inference...
eqsbc3r 3178 ~ eqsbc3 with set variable...
sbc3ang 3179 Distribution of class subs...
sbcel1gv 3180 Class substitution into a ...
sbcel2gv 3181 Class substitution into a ...
sbcimdv 3182 Substitution analog of The...
sbctt 3183 Substitution for a variabl...
sbcgf 3184 Substitution for a variabl...
sbc19.21g 3185 Substitution for a variabl...
sbcg 3186 Substitution for a variabl...
sbc2iegf 3187 Conversion of implicit sub...
sbc2ie 3188 Conversion of implicit sub...
sbc2iedv 3189 Conversion of implicit sub...
sbc3ie 3190 Conversion of implicit sub...
sbccomlem 3191 Lemma for ~ sbccom . (Con...
sbccom 3192 Commutative law for double...
sbcralt 3193 Interchange class substitu...
sbcrext 3194 Interchange class substitu...
sbcralg 3195 Interchange class substitu...
sbcrexg 3196 Interchange class substitu...
sbcreug 3197 Interchange class substitu...
sbcabel 3198 Interchange class substitu...
rspsbc 3199 Restricted quantifier vers...
rspsbca 3200 Restricted quantifier vers...
rspesbca 3201 Existence form of ~ rspsbc...
spesbc 3202 Existence form of ~ spsbc ...
spesbcd 3203 form of ~ spsbc . (Contri...
sbcth2 3204 A substitution into a theo...
ra5 3205 Restricted quantifier vers...
rmo2 3206 Alternate definition of re...
rmo2i 3207 Condition implying restric...
rmo3 3208 Restricted "at most one" u...
rmob 3209 Consequence of "at most on...
rmoi 3210 Consequence of "at most on...
csb2 3213 Alternate expression for t...
csbeq1 3214 Analog of ~ dfsbcq for pro...
cbvcsb 3215 Change bound variables in ...
cbvcsbv 3216 Change the bound variable ...
csbeq1d 3217 Equality deduction for pro...
csbid 3218 Analog of ~ sbid for prope...
csbeq1a 3219 Equality theorem for prope...
csbco 3220 Composition law for chaine...
csbexg 3221 The existence of proper su...
csbex 3222 The existence of proper su...
csbtt 3223 Substitution doesn't affec...
csbconstgf 3224 Substitution doesn't affec...
csbconstg 3225 Substitution doesn't affec...
sbcel12g 3226 Distribute proper substitu...
sbceqg 3227 Distribute proper substitu...
sbcnel12g 3228 Distribute proper substitu...
sbcne12g 3229 Distribute proper substitu...
sbcel1g 3230 Move proper substitution i...
sbceq1g 3231 Move proper substitution t...
sbcel2g 3232 Move proper substitution i...
sbceq2g 3233 Move proper substitution t...
csbcomg 3234 Commutative law for double...
csbeq2d 3235 Formula-building deduction...
csbeq2dv 3236 Formula-building deduction...
csbeq2i 3237 Formula-building inference...
csbvarg 3238 The proper substitution of...
sbccsbg 3239 Substitution into a wff ex...
sbccsb2g 3240 Substitution into a wff ex...
nfcsb1d 3241 Bound-variable hypothesis ...
nfcsb1 3242 Bound-variable hypothesis ...
nfcsb1v 3243 Bound-variable hypothesis ...
nfcsbd 3244 Deduction version of ~ nfc...
nfcsb 3245 Bound-variable hypothesis ...
csbhypf 3246 Introduce an explicit subs...
csbiebt 3247 Conversion of implicit sub...
csbiedf 3248 Conversion of implicit sub...
csbieb 3249 Bidirectional conversion b...
csbiebg 3250 Bidirectional conversion b...
csbiegf 3251 Conversion of implicit sub...
csbief 3252 Conversion of implicit sub...
csbied 3253 Conversion of implicit sub...
csbied2 3254 Conversion of implicit sub...
csbie2t 3255 Conversion of implicit sub...
csbie2 3256 Conversion of implicit sub...
csbie2g 3257 Conversion of implicit sub...
sbcnestgf 3258 Nest the composition of tw...
csbnestgf 3259 Nest the composition of tw...
sbcnestg 3260 Nest the composition of tw...
csbnestg 3261 Nest the composition of tw...
csbnestgOLD 3262 Nest the composition of tw...
csbnest1g 3263 Nest the composition of tw...
csbidmg 3264 Idempotent law for class s...
sbcco3g 3265 Composition of two substit...
sbcco3gOLD 3266 Composition of two substit...
csbco3g 3267 Composition of two class s...
rspcsbela 3268 Special case related to ~ ...
sbnfc2 3269 Two ways of expressing " `...
csbabg 3270 Move substitution into a c...
cbvralcsf 3271 A more general version of ...
cbvrexcsf 3272 A more general version of ...
cbvreucsf 3273 A more general version of ...
cbvrabcsf 3274 A more general version of ...
cbvralv2 3275 Rule used to change the bo...
cbvrexv2 3276 Rule used to change the bo...
difjust 3282 Soundness justification th...
unjust 3284 Soundness justification th...
injust 3286 Soundness justification th...
dfin5 3288 Alternate definition for t...
dfdif2 3289 Alternate definition of cl...
eldif 3290 Expansion of membership in...
eldifd 3291 If a class is in one class...
eldifad 3292 If a class is in the diffe...
eldifbd 3293 If a class is in the diffe...
dfss 3295 Variant of subclass defini...
dfss2 3297 Alternate definition of th...
dfss3 3298 Alternate definition of su...
dfss2f 3299 Equivalence for subclass r...
dfss3f 3300 Equivalence for subclass r...
nfss 3301 If ` x ` is not free in ` ...
ssel 3302 Membership relationships f...
ssel2 3303 Membership relationships f...
sseli 3304 Membership inference from ...
sselii 3305 Membership inference from ...
sseldi 3306 Membership inference from ...
sseld 3307 Membership deduction from ...
sselda 3308 Membership deduction from ...
sseldd 3309 Membership inference from ...
ssneld 3310 If a class is not in anoth...
ssneldd 3311 If an element is not in a ...
ssriv 3312 Inference rule based on su...
ssrd 3313 Deduction rule based on su...
ssrdv 3314 Deduction rule based on su...
sstr2 3315 Transitivity of subclasses...
sstr 3316 Transitivity of subclasses...
sstri 3317 Subclass transitivity infe...
sstrd 3318 Subclass transitivity dedu...
syl5ss 3319 Subclass transitivity dedu...
syl6ss 3320 Subclass transitivity dedu...
sylan9ss 3321 A subclass transitivity de...
sylan9ssr 3322 A subclass transitivity de...
eqss 3323 The subclass relationship ...
eqssi 3324 Infer equality from two su...
eqssd 3325 Equality deduction from tw...
eqrd 3326 Deduce equality of classes...
ssid 3327 Any class is a subclass of...
ssv 3328 Any class is a subclass of...
sseq1 3329 Equality theorem for subcl...
sseq2 3330 Equality theorem for the s...
sseq12 3331 Equality theorem for the s...
sseq1i 3332 An equality inference for ...
sseq2i 3333 An equality inference for ...
sseq12i 3334 An equality inference for ...
sseq1d 3335 An equality deduction for ...
sseq2d 3336 An equality deduction for ...
sseq12d 3337 An equality deduction for ...
eqsstri 3338 Substitution of equality i...
eqsstr3i 3339 Substitution of equality i...
sseqtri 3340 Substitution of equality i...
sseqtr4i 3341 Substitution of equality i...
eqsstrd 3342 Substitution of equality i...
eqsstr3d 3343 Substitution of equality i...
sseqtrd 3344 Substitution of equality i...
sseqtr4d 3345 Substitution of equality i...
3sstr3i 3346 Substitution of equality i...
3sstr4i 3347 Substitution of equality i...
3sstr3g 3348 Substitution of equality i...
3sstr4g 3349 Substitution of equality i...
3sstr3d 3350 Substitution of equality i...
3sstr4d 3351 Substitution of equality i...
syl5eqss 3352 B chained subclass and equ...
syl5eqssr 3353 B chained subclass and equ...
syl6sseq 3354 A chained subclass and equ...
syl6sseqr 3355 A chained subclass and equ...
syl5sseq 3356 Subclass transitivity dedu...
syl5sseqr 3357 Subclass transitivity dedu...
syl6eqss 3358 A chained subclass and equ...
syl6eqssr 3359 A chained subclass and equ...
eqimss 3360 Equality implies the subcl...
eqimss2 3361 Equality implies the subcl...
eqimssi 3362 Infer subclass relationshi...
eqimss2i 3363 Infer subclass relationshi...
nssne1 3364 Two classes are different ...
nssne2 3365 Two classes are different ...
nss 3366 Negation of subclass relat...
ssralv 3367 Quantification restricted ...
ssrexv 3368 Existential quantification...
ralss 3369 Restricted universal quant...
rexss 3370 Restricted existential qua...
ss2ab 3371 Class abstractions in a su...
abss 3372 Class abstraction in a sub...
ssab 3373 Subclass of a class abstra...
ssabral 3374 The relation for a subclas...
ss2abi 3375 Inference of abstraction s...
ss2abdv 3376 Deduction of abstraction s...
abssdv 3377 Deduction of abstraction s...
abssi 3378 Inference of abstraction s...
ss2rab 3379 Restricted abstraction cla...
rabss 3380 Restricted class abstracti...
ssrab 3381 Subclass of a restricted c...
ssrabdv 3382 Subclass of a restricted c...
rabssdv 3383 Subclass of a restricted c...
ss2rabdv 3384 Deduction of restricted ab...
ss2rabi 3385 Inference of restricted ab...
rabss2 3386 Subclass law for restricte...
ssab2 3387 Subclass relation for the ...
ssrab2 3388 Subclass relation for a re...
ssrabeq 3389 If the restricting class o...
rabssab 3390 A restricted class is a su...
uniiunlem 3391 A subset relationship usef...
dfpss2 3392 Alternate definition of pr...
dfpss3 3393 Alternate definition of pr...
psseq1 3394 Equality theorem for prope...
psseq2 3395 Equality theorem for prope...
psseq1i 3396 An equality inference for ...
psseq2i 3397 An equality inference for ...
psseq12i 3398 An equality inference for ...
psseq1d 3399 An equality deduction for ...
psseq2d 3400 An equality deduction for ...
psseq12d 3401 An equality deduction for ...
pssss 3402 A proper subclass is a sub...
pssne 3403 Two classes in a proper su...
pssssd 3404 Deduce subclass from prope...
pssned 3405 Proper subclasses are uneq...
sspss 3406 Subclass in terms of prope...
pssirr 3407 Proper subclass is irrefle...
pssn2lp 3408 Proper subclass has no 2-c...
sspsstri 3409 Two ways of stating tricho...
ssnpss 3410 Partial trichotomy law for...
psstr 3411 Transitive law for proper ...
sspsstr 3412 Transitive law for subclas...
psssstr 3413 Transitive law for subclas...
psstrd 3414 Proper subclass inclusion ...
sspsstrd 3415 Transitivity involving sub...
psssstrd 3416 Transitivity involving sub...
npss 3417 A class is not a proper su...
difeq1 3418 Equality theorem for class...
difeq2 3419 Equality theorem for class...
difeq12 3420 Equality theorem for class...
difeq1i 3421 Inference adding differenc...
difeq2i 3422 Inference adding differenc...
difeq12i 3423 Equality inference for cla...
difeq1d 3424 Deduction adding differenc...
difeq2d 3425 Deduction adding differenc...
difeq12d 3426 Equality deduction for cla...
difeqri 3427 Inference from membership ...
nfdif 3428 Bound-variable hypothesis ...
eldifi 3429 Implication of membership ...
eldifn 3430 Implication of membership ...
elndif 3431 A set does not belong to a...
neldif 3432 Implication of membership ...
difdif 3433 Double class difference. ...
difss 3434 Subclass relationship for ...
difssd 3435 A difference of two classe...
difss2 3436 If a class is contained in...
difss2d 3437 If a class is contained in...
ssdifss 3438 Preservation of a subclass...
ddif 3439 Double complement under un...
ssconb 3440 Contraposition law for sub...
sscon 3441 Contraposition law for sub...
ssdif 3442 Difference law for subsets...
ssdifd 3443 If ` A ` is contained in `...
sscond 3444 If ` A ` is contained in `...
ssdifssd 3445 If ` A ` is contained in `...
ssdif2d 3446 If ` A ` is contained in `...
raldifb 3447 Restricted universal quant...
elun 3448 Expansion of membership in...
uneqri 3449 Inference from membership ...
unidm 3450 Idempotent law for union o...
uncom 3451 Commutative law for union ...
equncom 3452 If a class equals the unio...
equncomi 3453 Inference form of ~ equnco...
uneq1 3454 Equality theorem for union...
uneq2 3455 Equality theorem for the u...
uneq12 3456 Equality theorem for union...
uneq1i 3457 Inference adding union to ...
uneq2i 3458 Inference adding union to ...
uneq12i 3459 Equality inference for uni...
uneq1d 3460 Deduction adding union to ...
uneq2d 3461 Deduction adding union to ...
uneq12d 3462 Equality deduction for uni...
nfun 3463 Bound-variable hypothesis ...
unass 3464 Associative law for union ...
un12 3465 A rearrangement of union. ...
un23 3466 A rearrangement of union. ...
un4 3467 A rearrangement of the uni...
unundi 3468 Union distributes over its...
unundir 3469 Union distributes over its...
ssun1 3470 Subclass relationship for ...
ssun2 3471 Subclass relationship for ...
ssun3 3472 Subclass law for union of ...
ssun4 3473 Subclass law for union of ...
elun1 3474 Membership law for union o...
elun2 3475 Membership law for union o...
unss1 3476 Subclass law for union of ...
ssequn1 3477 A relationship between sub...
unss2 3478 Subclass law for union of ...
unss12 3479 Subclass law for union of ...
ssequn2 3480 A relationship between sub...
unss 3481 The union of two subclasse...
unssi 3482 An inference showing the u...
unssd 3483 A deduction showing the un...
unssad 3484 If ` ( A u. B ) ` is conta...
unssbd 3485 If ` ( A u. B ) ` is conta...
ssun 3486 A condition that implies i...
rexun 3487 Restricted existential qua...
ralunb 3488 Restricted quantification ...
ralun 3489 Restricted quantification ...
elin 3490 Expansion of membership in...
elin2 3491 Membership in a class defi...
elin3 3492 Membership in a class defi...
incom 3493 Commutative law for inters...
ineqri 3494 Inference from membership ...
ineq1 3495 Equality theorem for inter...
ineq2 3496 Equality theorem for inter...
ineq12 3497 Equality theorem for inter...
ineq1i 3498 Equality inference for int...
ineq2i 3499 Equality inference for int...
ineq12i 3500 Equality inference for int...
ineq1d 3501 Equality deduction for int...
ineq2d 3502 Equality deduction for int...
ineq12d 3503 Equality deduction for int...
ineqan12d 3504 Equality deduction for int...
dfss1 3505 A frequently-used variant ...
dfss5 3506 Another definition of subc...
nfin 3507 Bound-variable hypothesis ...
csbing 3508 Distribute proper substitu...
rabbi2dva 3509 Deduction from a wff to a ...
inidm 3510 Idempotent law for interse...
inass 3511 Associative law for inters...
in12 3512 A rearrangement of interse...
in32 3513 A rearrangement of interse...
in13 3514 A rearrangement of interse...
in31 3515 A rearrangement of interse...
inrot 3516 Rotate the intersection of...
in4 3517 Rearrangement of intersect...
inindi 3518 Intersection distributes o...
inindir 3519 Intersection distributes o...
sseqin2 3520 A relationship between sub...
inss1 3521 The intersection of two cl...
inss2 3522 The intersection of two cl...
ssin 3523 Subclass of intersection. ...
ssini 3524 An inference showing that ...
ssind 3525 A deduction showing that a...
ssrin 3526 Add right intersection to ...
sslin 3527 Add left intersection to s...
ss2in 3528 Intersection of subclasses...
ssinss1 3529 Intersection preserves sub...
inss 3530 Inclusion of an intersecti...
unabs 3531 Absorption law for union. ...
inabs 3532 Absorption law for interse...
nssinpss 3533 Negation of subclass expre...
nsspssun 3534 Negation of subclass expre...
dfss4 3535 Subclass defined in terms ...
dfun2 3536 An alternate definition of...
dfin2 3537 An alternate definition of...
difin 3538 Difference with intersecti...
dfun3 3539 Union defined in terms of ...
dfin3 3540 Intersection defined in te...
dfin4 3541 Alternate definition of th...
invdif 3542 Intersection with universa...
indif 3543 Intersection with class di...
indif2 3544 Bring an intersection in a...
indif1 3545 Bring an intersection in a...
indifcom 3546 Commutation law for inters...
indi 3547 Distributive law for inter...
undi 3548 Distributive law for union...
indir 3549 Distributive law for inter...
undir 3550 Distributive law for union...
unineq 3551 Infer equality from equali...
uneqin 3552 Equality of union and inte...
difundi 3553 Distributive law for class...
difundir 3554 Distributive law for class...
difindi 3555 Distributive law for class...
difindir 3556 Distributive law for class...
indifdir 3557 Distribute intersection ov...
difdif2 3558 Set difference with a set ...
undm 3559 De Morgan's law for union....
indm 3560 De Morgan's law for inters...
difun1 3561 A relationship involving d...
undif3 3562 An equality involving clas...
difin2 3563 Represent a set difference...
dif32 3564 Swap second and third argu...
difabs 3565 Absorption-like law for cl...
symdif1 3566 Two ways to express symmet...
symdif2 3567 Two ways to express symmet...
unab 3568 Union of two class abstrac...
inab 3569 Intersection of two class ...
difab 3570 Difference of two class ab...
notab 3571 A class builder defined by...
unrab 3572 Union of two restricted cl...
inrab 3573 Intersection of two restri...
inrab2 3574 Intersection with a restri...
difrab 3575 Difference of two restrict...
dfrab2 3576 Alternate definition of re...
dfrab3 3577 Alternate definition of re...
notrab 3578 Complementation of restric...
dfrab3ss 3579 Restricted class abstracti...
rabun2 3580 Abstraction restricted to ...
reuss2 3581 Transfer uniqueness to a s...
reuss 3582 Transfer uniqueness to a s...
reuun1 3583 Transfer uniqueness to a s...
reuun2 3584 Transfer uniqueness to a s...
reupick 3585 Restricted uniqueness "pic...
reupick3 3586 Restricted uniqueness "pic...
reupick2 3587 Restricted uniqueness "pic...
dfnul2 3590 Alternate definition of th...
dfnul3 3591 Alternate definition of th...
noel 3592 The empty set has no eleme...
n0i 3593 If a set has elements, it ...
ne0i 3594 If a set has elements, it ...
vn0 3595 The universal class is not...
n0f 3596 A nonempty class has at le...
n0 3597 A nonempty class has at le...
neq0 3598 A nonempty class has at le...
reximdva0 3599 Restricted existence deduc...
n0moeu 3600 A case of equivalence of "...
rex0 3601 Vacuous existential quanti...
eq0 3602 The empty set has no eleme...
eqv 3603 The universe contains ever...
0el 3604 Membership of the empty se...
abvor0 3605 The class builder of a wff...
abn0 3606 Nonempty class abstraction...
rabn0 3607 Non-empty restricted class...
rab0 3608 Any restricted class abstr...
rabeq0 3609 Condition for a restricted...
rabxm 3610 Law of excluded middle, in...
rabnc 3611 Law of noncontradiction, i...
un0 3612 The union of a class with ...
in0 3613 The intersection of a clas...
inv1 3614 The intersection of a clas...
unv 3615 The union of a class with ...
0ss 3616 The null set is a subset o...
ss0b 3617 Any subset of the empty se...
ss0 3618 Any subset of the empty se...
sseq0 3619 A subclass of an empty cla...
ssn0 3620 A class with a nonempty su...
abf 3621 A class builder with a fal...
eq0rdv 3622 Deduction rule for equalit...
un00 3623 Two classes are empty iff ...
vss 3624 Only the universal class h...
0pss 3625 The null set is a proper s...
npss0 3626 No set is a proper subset ...
pssv 3627 Any non-universal class is...
disj 3628 Two ways of saying that tw...
disjr 3629 Two ways of saying that tw...
disj1 3630 Two ways of saying that tw...
reldisj 3631 Two ways of saying that tw...
disj3 3632 Two ways of saying that tw...
disjne 3633 Members of disjoint sets a...
disjel 3634 A set can't belong to both...
disj2 3635 Two ways of saying that tw...
disj4 3636 Two ways of saying that tw...
ssdisj 3637 Intersection with a subcla...
disjpss 3638 A class is a proper subset...
undisj1 3639 The union of disjoint clas...
undisj2 3640 The union of disjoint clas...
ssindif0 3641 Subclass expressed in term...
inelcm 3642 The intersection of classe...
minel 3643 A minimum element of a cla...
undif4 3644 Distribute union over diff...
disjssun 3645 Subset relation for disjoi...
ssdif0 3646 Subclass expressed in term...
vdif0 3647 Universal class equality i...
difrab0eq 3648 If the difference between ...
pssdifn0 3649 A proper subclass has a no...
pssdif 3650 A proper subclass has a no...
ssnelpss 3651 A subclass missing a membe...
ssnelpssd 3652 Subclass inclusion with on...
pssnel 3653 A proper subclass has a me...
difin0ss 3654 Difference, intersection, ...
inssdif0 3655 Intersection, subclass, an...
difid 3656 The difference between a c...
difidALT 3657 The difference between a c...
dif0 3658 The difference between a c...
0dif 3659 The difference between the...
disjdif 3660 A class and its relative c...
difin0 3661 The difference of a class ...
undifv 3662 The union of a class and i...
undif1 3663 Absorption of difference b...
undif2 3664 Absorption of difference b...
undifabs 3665 Absorption of difference b...
inundif 3666 The intersection and class...
difun2 3667 Absorption of union by dif...
undif 3668 Union of complementary par...
ssdifin0 3669 A subset of a difference d...
ssdifeq0 3670 A class is a subclass of i...
ssundif 3671 A condition equivalent to ...
difcom 3672 Swap the arguments of a cl...
pssdifcom1 3673 Two ways to express overla...
pssdifcom2 3674 Two ways to express non-co...
difdifdir 3675 Distributive law for class...
uneqdifeq 3676 Two ways to say that ` A `...
r19.2z 3677 Theorem 19.2 of [Margaris]...
r19.2zb 3678 A response to the notion t...
r19.3rz 3679 Restricted quantification ...
r19.28z 3680 Restricted quantifier vers...
r19.3rzv 3681 Restricted quantification ...
r19.9rzv 3682 Restricted quantification ...
r19.28zv 3683 Restricted quantifier vers...
r19.37zv 3684 Restricted quantifier vers...
r19.45zv 3685 Restricted version of Theo...
r19.27z 3686 Restricted quantifier vers...
r19.27zv 3687 Restricted quantifier vers...
r19.36zv 3688 Restricted quantifier vers...
rzal 3689 Vacuous quantification is ...
rexn0 3690 Restricted existential qua...
ralidm 3691 Idempotent law for restric...
ral0 3692 Vacuous universal quantifi...
rgenz 3693 Generalization rule that e...
ralf0 3694 The quantification of a fa...
raaan 3695 Rearrange restricted quant...
raaanv 3696 Rearrange restricted quant...
sbss 3697 Set substitution into the ...
sbcss 3698 Distribute proper substitu...
dfif2 3701 An alternate definition of...
dfif6 3702 An alternate definition of...
ifeq1 3703 Equality theorem for condi...
ifeq2 3704 Equality theorem for condi...
iftrue 3705 Value of the conditional o...
iffalse 3706 Value of the conditional o...
ifnefalse 3707 When values are unequal, b...
ifsb 3708 Distribute a function over...
dfif3 3709 Alternate definition of th...
dfif4 3710 Alternate definition of th...
dfif5 3711 Alternate definition of th...
ifeq12 3712 Equality theorem for condi...
ifeq1d 3713 Equality deduction for con...
ifeq2d 3714 Equality deduction for con...
ifeq12d 3715 Equality deduction for con...
ifbi 3716 Equivalence theorem for co...
ifbid 3717 Equivalence deduction for ...
ifbieq2i 3718 Equivalence/equality infer...
ifbieq2d 3719 Equivalence/equality deduc...
ifbieq12i 3720 Equivalence deduction for ...
ifbieq12d 3721 Equivalence deduction for ...
nfifd 3722 Deduction version of ~ nfi...
nfif 3723 Bound-variable hypothesis ...
ifeq1da 3724 Conditional equality. (Co...
ifeq2da 3725 Conditional equality. (Co...
ifclda 3726 Conditional closure. (Con...
csbifg 3727 Distribute proper substitu...
elimif 3728 Elimination of a condition...
ifbothda 3729 A wff ` th ` containing a ...
ifboth 3730 A wff ` th ` containing a ...
ifid 3731 Identical true and false a...
eqif 3732 Expansion of an equality w...
elif 3733 Membership in a conditiona...
ifel 3734 Membership of a conditiona...
ifcl 3735 Membership (closure) of a ...
ifeqor 3736 The possible values of a c...
ifnot 3737 Negating the first argumen...
ifan 3738 Rewrite a conjunction in a...
ifor 3739 Rewrite a disjunction in a...
dedth 3740 Weak deduction theorem tha...
dedth2h 3741 Weak deduction theorem eli...
dedth3h 3742 Weak deduction theorem eli...
dedth4h 3743 Weak deduction theorem eli...
dedth2v 3744 Weak deduction theorem for...
dedth3v 3745 Weak deduction theorem for...
dedth4v 3746 Weak deduction theorem for...
elimhyp 3747 Eliminate a hypothesis con...
elimhyp2v 3748 Eliminate a hypothesis con...
elimhyp3v 3749 Eliminate a hypothesis con...
elimhyp4v 3750 Eliminate a hypothesis con...
elimel 3751 Eliminate a membership hyp...
elimdhyp 3752 Version of ~ elimhyp where...
keephyp 3753 Transform a hypothesis ` p...
keephyp2v 3754 Keep a hypothesis containi...
keephyp3v 3755 Keep a hypothesis containi...
keepel 3756 Keep a membership hypothes...
ifex 3757 Conditional operator exist...
ifexg 3758 Conditional operator exist...
pwjust 3760 Soundness justification th...
pweq 3762 Equality theorem for power...
pweqi 3763 Equality inference for pow...
pweqd 3764 Equality deduction for pow...
elpw 3765 Membership in a power clas...
elpwg 3766 Membership in a power clas...
elpwi 3767 Subset relation implied by...
elpwid 3768 An element of a power clas...
elelpwi 3769 If ` A ` belongs to a part...
nfpw 3770 Bound-variable hypothesis ...
pwidg 3771 Membership of the original...
pwid 3772 A set is a member of its p...
pwss 3773 Subclass relationship for ...
snjust 3779 Soundness justification th...
sneq 3785 Equality theorem for singl...
sneqi 3786 Equality inference for sin...
sneqd 3787 Equality deduction for sin...
dfsn2 3788 Alternate definition of si...
elsn 3789 There is only one element ...
dfpr2 3790 Alternate definition of un...
elprg 3791 A member of an unordered p...
elpr 3792 A member of an unordered p...
elpr2 3793 A member of an unordered p...
elpri 3794 If a class is an element o...
nelpri 3795 If an element doesn't matc...
elsncg 3796 There is only one element ...
elsnc 3797 There is only one element ...
elsni 3798 There is only one element ...
snidg 3799 A set is a member of its s...
snidb 3800 A class is a set iff it is...
snid 3801 A set is a member of its s...
elsnc2g 3802 There is only one element ...
elsnc2 3803 There is only one element ...
ralsns 3804 Substitution expressed in ...
rexsns 3805 Restricted existential qua...
ralsng 3806 Substitution expressed in ...
rexsng 3807 Restricted existential qua...
exsnrex 3808 There is a set being the e...
ralsn 3809 Convert a quantification o...
rexsn 3810 Restricted existential qua...
eltpg 3811 Members of an unordered tr...
eltpi 3812 A member of an unordered t...
eltp 3813 A member of an unordered t...
dftp2 3814 Alternate definition of un...
nfpr 3815 Bound-variable hypothesis ...
ifpr 3816 Membership of a conditiona...
ralprg 3817 Convert a quantification o...
rexprg 3818 Convert a quantification o...
raltpg 3819 Convert a quantification o...
rextpg 3820 Convert a quantification o...
ralpr 3821 Convert a quantification o...
rexpr 3822 Convert an existential qua...
raltp 3823 Convert a quantification o...
rextp 3824 Convert a quantification o...
sbcsng 3825 Substitution expressed in ...
nfsn 3826 Bound-variable hypothesis ...
csbsng 3827 Distribute proper substitu...
disjsn 3828 Intersection with the sing...
disjsn2 3829 Intersection of distinct s...
disjpr2 3830 The intersection of distin...
snprc 3831 The singleton of a proper ...
r19.12sn 3832 Special case of ~ r19.12 w...
rabsn 3833 Condition where a restrict...
rabrsn 3834 A restricted class abstrac...
euabsn2 3835 Another way to express exi...
euabsn 3836 Another way to express exi...
reusn 3837 A way to express restricte...
absneu 3838 Restricted existential uni...
rabsneu 3839 Restricted existential uni...
eusn 3840 Two ways to express " ` A ...
rabsnt 3841 Truth implied by equality ...
prcom 3842 Commutative law for unorde...
preq1 3843 Equality theorem for unord...
preq2 3844 Equality theorem for unord...
preq12 3845 Equality theorem for unord...
preq1i 3846 Equality inference for uno...
preq2i 3847 Equality inference for uno...
preq12i 3848 Equality inference for uno...
preq1d 3849 Equality deduction for uno...
preq2d 3850 Equality deduction for uno...
preq12d 3851 Equality deduction for uno...
tpeq1 3852 Equality theorem for unord...
tpeq2 3853 Equality theorem for unord...
tpeq3 3854 Equality theorem for unord...
tpeq1d 3855 Equality theorem for unord...
tpeq2d 3856 Equality theorem for unord...
tpeq3d 3857 Equality theorem for unord...
tpeq123d 3858 Equality theorem for unord...
tprot 3859 Rotation of the elements o...
tpcoma 3860 Swap 1st and 2nd members o...
tpcomb 3861 Swap 2nd and 3rd members o...
tpass 3862 Split off the first elemen...
qdass 3863 Two ways to write an unord...
qdassr 3864 Two ways to write an unord...
tpidm12 3865 Unordered triple ` { A , A...
tpidm13 3866 Unordered triple ` { A , B...
tpidm23 3867 Unordered triple ` { A , B...
tpidm 3868 Unordered triple ` { A , A...
tppreq3 3869 An unordered triple is an ...
prid1g 3870 An unordered pair contains...
prid2g 3871 An unordered pair contains...
prid1 3872 An unordered pair contains...
prid2 3873 An unordered pair contains...
prprc1 3874 A proper class vanishes in...
prprc2 3875 A proper class vanishes in...
prprc 3876 An unordered pair containi...
tpid1 3877 One of the three elements ...
tpid2 3878 One of the three elements ...
tpid3g 3879 Closed theorem form of ~ t...
tpid3 3880 One of the three elements ...
snnzg 3881 The singleton of a set is ...
snnz 3882 The singleton of a set is ...
prnz 3883 A pair containing a set is...
prnzg 3884 A pair containing a set is...
tpnz 3885 A triplet containing a set...
snss 3886 The singleton of an elemen...
eldifsn 3887 Membership in a set with a...
eldifsni 3888 Membership in a set with a...
neldifsn 3889 ` A ` is not in ` ( B \ { ...
neldifsnd 3890 ` A ` is not in ` ( B \ { ...
rexdifsn 3891 Restricted existential qua...
snssg 3892 The singleton of an elemen...
difsn 3893 An element not in a set ca...
difprsnss 3894 Removal of a singleton fro...
difprsn1 3895 Removal of a singleton fro...
difprsn2 3896 Removal of a singleton fro...
diftpsn3 3897 Removal of a singleton fro...
tpprceq3 3898 An unordered triple is an ...
tppreqb 3899 An unordered triple is an ...
difsnb 3900 ` ( B \ { A } ) ` equals `...
difsnpss 3901 ` ( B \ { A } ) ` is a pro...
snssi 3902 The singleton of an elemen...
snssd 3903 The singleton of an elemen...
difsnid 3904 If we remove a single elem...
pw0 3905 Compute the power set of t...
pwpw0 3906 Compute the power set of t...
snsspr1 3907 A singleton is a subset of...
snsspr2 3908 A singleton is a subset of...
snsstp1 3909 A singleton is a subset of...
snsstp2 3910 A singleton is a subset of...
snsstp3 3911 A singleton is a subset of...
prss 3912 A pair of elements of a cl...
prssg 3913 A pair of elements of a cl...
prssi 3914 A pair of elements of a cl...
prsspwg 3915 An unordered pair belongs ...
prsspwgOLD 3916 Obsolete version of ~ prss...
sssn 3917 The subsets of a singleton...
ssunsn2 3918 The property of being sand...
ssunsn 3919 Possible values for a set ...
eqsn 3920 Two ways to express that a...
ssunpr 3921 Possible values for a set ...
sspr 3922 The subsets of a pair. (C...
sstp 3923 The subsets of a triple. ...
tpss 3924 A triplet of elements of a...
tpssi 3925 A triple of elements of a ...
sneqr 3926 If the singletons of two s...
snsssn 3927 If a singleton is a subset...
sneqrg 3928 Closed form of ~ sneqr . ...
sneqbg 3929 Two singletons of sets are...
snsspw 3930 The singleton of a class i...
prsspw 3931 An unordered pair belongs ...
preqr1 3932 Reverse equality lemma for...
preqr2 3933 Reverse equality lemma for...
preq12b 3934 Equality relationship for ...
prel12 3935 Equality of two unordered ...
opthpr 3936 A way to represent ordered...
preq12bg 3937 Closed form of ~ preq12b ....
prneimg 3938 Two pairs are not equal if...
prnebg 3939 A (proper) pair is not equ...
preqsn 3940 Equivalence for a pair equ...
dfopif 3941 Rewrite ~ df-op using ` if...
dfopg 3942 Value of the ordered pair ...
dfop 3943 Value of an ordered pair w...
opeq1 3944 Equality theorem for order...
opeq2 3945 Equality theorem for order...
opeq12 3946 Equality theorem for order...
opeq1i 3947 Equality inference for ord...
opeq2i 3948 Equality inference for ord...
opeq12i 3949 Equality inference for ord...
opeq1d 3950 Equality deduction for ord...
opeq2d 3951 Equality deduction for ord...
opeq12d 3952 Equality deduction for ord...
oteq1 3953 Equality theorem for order...
oteq2 3954 Equality theorem for order...
oteq3 3955 Equality theorem for order...
oteq1d 3956 Equality deduction for ord...
oteq2d 3957 Equality deduction for ord...
oteq3d 3958 Equality deduction for ord...
oteq123d 3959 Equality deduction for ord...
nfop 3960 Bound-variable hypothesis ...
nfopd 3961 Deduction version of bound...
opid 3962 The ordered pair ` <. A , ...
ralunsn 3963 Restricted quantification ...
2ralunsn 3964 Double restricted quantifi...
opprc 3965 Expansion of an ordered pa...
opprc1 3966 Expansion of an ordered pa...
opprc2 3967 Expansion of an ordered pa...
oprcl 3968 If an ordered pair has an ...
pwsn 3969 The power set of a singlet...
pwsnALT 3970 The power set of a singlet...
pwpr 3971 The power set of an unorde...
pwtp 3972 The power set of an unorde...
pwpwpw0 3973 Compute the power set of t...
pwv 3974 The power class of the uni...
dfuni2 3977 Alternate definition of cl...
eluni 3978 Membership in class union....
eluni2 3979 Membership in class union....
elunii 3980 Membership in class union....
nfuni 3981 Bound-variable hypothesis ...
nfunid 3982 Deduction version of ~ nfu...
csbunig 3983 Distribute proper substitu...
unieq 3984 Equality theorem for class...
unieqi 3985 Inference of equality of t...
unieqd 3986 Deduction of equality of t...
eluniab 3987 Membership in union of a c...
elunirab 3988 Membership in union of a c...
unipr 3989 The union of a pair is the...
uniprg 3990 The union of a pair is the...
unisn 3991 A set equals the union of ...
unisng 3992 A set equals the union of ...
dfnfc2 3993 An alternative statement o...
uniun 3994 The class union of the uni...
uniin 3995 The class union of the int...
uniss 3996 Subclass relationship for ...
ssuni 3997 Subclass relationship for ...
unissi 3998 Subclass relationship for ...
unissd 3999 Subclass relationship for ...
uni0b 4000 The union of a set is empt...
uni0c 4001 The union of a set is empt...
uni0 4002 The union of the empty set...
elssuni 4003 An element of a class is a...
unissel 4004 Condition turning a subcla...
unissb 4005 Relationship involving mem...
uniss2 4006 A subclass condition on th...
unidif 4007 If the difference ` A \ B ...
ssunieq 4008 Relationship implying unio...
unimax 4009 Any member of a class is t...
dfint2 4012 Alternate definition of cl...
inteq 4013 Equality law for intersect...
inteqi 4014 Equality inference for cla...
inteqd 4015 Equality deduction for cla...
elint 4016 Membership in class inters...
elint2 4017 Membership in class inters...
elintg 4018 Membership in class inters...
elinti 4019 Membership in class inters...
nfint 4020 Bound-variable hypothesis ...
elintab 4021 Membership in the intersec...
elintrab 4022 Membership in the intersec...
elintrabg 4023 Membership in the intersec...
int0 4024 The intersection of the em...
intss1 4025 An element of a class incl...
ssint 4026 Subclass of a class inters...
ssintab 4027 Subclass of the intersecti...
ssintub 4028 Subclass of the least uppe...
ssmin 4029 Subclass of the minimum va...
intmin 4030 Any member of a class is t...
intss 4031 Intersection of subclasses...
intssuni 4032 The intersection of a none...
ssintrab 4033 Subclass of the intersecti...
unissint 4034 If the union of a class is...
intssuni2 4035 Subclass relationship for ...
intminss 4036 Under subset ordering, the...
intmin2 4037 Any set is the smallest of...
intmin3 4038 Under subset ordering, the...
intmin4 4039 Elimination of a conjunct ...
intab 4040 The intersection of a spec...
int0el 4041 The intersection of a clas...
intun 4042 The class intersection of ...
intpr 4043 The intersection of a pair...
intprg 4044 The intersection of a pair...
intsng 4045 Intersection of a singleto...
intsn 4046 The intersection of a sing...
uniintsn 4047 Two ways to express " ` A ...
uniintab 4048 The union and the intersec...
intunsn 4049 Theorem joining a singleto...
rint0 4050 Relative intersection of a...
elrint 4051 Membership in a restricted...
elrint2 4052 Membership in a restricted...
eliun 4057 Membership in indexed unio...
eliin 4058 Membership in indexed inte...
iuncom 4059 Commutation of indexed uni...
iuncom4 4060 Commutation of union with ...
iunconst 4061 Indexed union of a constan...
iinconst 4062 Indexed intersection of a ...
iuniin 4063 Law combining indexed unio...
iunss1 4064 Subclass theorem for index...
iinss1 4065 Subclass theorem for index...
iuneq1 4066 Equality theorem for index...
iineq1 4067 Equality theorem for restr...
ss2iun 4068 Subclass theorem for index...
iuneq2 4069 Equality theorem for index...
iineq2 4070 Equality theorem for index...
iuneq2i 4071 Equality inference for ind...
iineq2i 4072 Equality inference for ind...
iineq2d 4073 Equality deduction for ind...
iuneq2dv 4074 Equality deduction for ind...
iineq2dv 4075 Equality deduction for ind...
iuneq1d 4076 Equality theorem for index...
iuneq12d 4077 Equality deduction for ind...
iuneq2d 4078 Equality deduction for ind...
nfiun 4079 Bound-variable hypothesis ...
nfiin 4080 Bound-variable hypothesis ...
nfiu1 4081 Bound-variable hypothesis ...
nfii1 4082 Bound-variable hypothesis ...
dfiun2g 4083 Alternate definition of in...
dfiin2g 4084 Alternate definition of in...
dfiun2 4085 Alternate definition of in...
dfiin2 4086 Alternate definition of in...
dfiunv2 4087 Define double indexed unio...
cbviun 4088 Rule used to change the bo...
cbviin 4089 Change bound variables in ...
cbviunv 4090 Rule used to change the bo...
cbviinv 4091 Change bound variables in ...
iunss 4092 Subset theorem for an inde...
ssiun 4093 Subset implication for an ...
ssiun2 4094 Identity law for subset of...
ssiun2s 4095 Subset relationship for an...
iunss2 4096 A subclass condition on th...
iunab 4097 The indexed union of a cla...
iunrab 4098 The indexed union of a res...
iunxdif2 4099 Indexed union with a class...
ssiinf 4100 Subset theorem for an inde...
ssiin 4101 Subset theorem for an inde...
iinss 4102 Subset implication for an ...
iinss2 4103 An indexed intersection is...
uniiun 4104 Class union in terms of in...
intiin 4105 Class intersection in term...
iunid 4106 An indexed union of single...
iun0 4107 An indexed union of the em...
0iun 4108 An empty indexed union is ...
0iin 4109 An empty indexed intersect...
viin 4110 Indexed intersection with ...
iunn0 4111 There is a non-empty class...
iinab 4112 Indexed intersection of a ...
iinrab 4113 Indexed intersection of a ...
iinrab2 4114 Indexed intersection of a ...
iunin2 4115 Indexed union of intersect...
iunin1 4116 Indexed union of intersect...
iinun2 4117 Indexed intersection of un...
iundif2 4118 Indexed union of class dif...
2iunin 4119 Rearrange indexed unions o...
iindif2 4120 Indexed intersection of cl...
iinin2 4121 Indexed intersection of in...
iinin1 4122 Indexed intersection of in...
elriin 4123 Elementhood in a relative ...
riin0 4124 Relative intersection of a...
riinn0 4125 Relative intersection of a...
riinrab 4126 Relative intersection of a...
iinxsng 4127 A singleton index picks ou...
iinxprg 4128 Indexed intersection with ...
iunxsng 4129 A singleton index picks ou...
iunxsn 4130 A singleton index picks ou...
iunun 4131 Separate a union in an ind...
iunxun 4132 Separate a union in the in...
iunxiun 4133 Separate an indexed union ...
iinuni 4134 A relationship involving u...
iununi 4135 A relationship involving u...
sspwuni 4136 Subclass relationship for ...
pwssb 4137 Two ways to express a coll...
elpwuni 4138 Relationship for power cla...
iinpw 4139 The power class of an inte...
iunpwss 4140 Inclusion of an indexed un...
rintn0 4141 Relative intersection of a...
dfdisj2 4144 Alternate definition for d...
disjss2 4145 If each element of a colle...
disjeq2 4146 Equality theorem for disjo...
disjeq2dv 4147 Equality deduction for dis...
disjss1 4148 A subset of a disjoint col...
disjeq1 4149 Equality theorem for disjo...
disjeq1d 4150 Equality theorem for disjo...
disjeq12d 4151 Equality theorem for disjo...
cbvdisj 4152 Change bound variables in ...
cbvdisjv 4153 Change bound variables in ...
nfdisj 4154 Bound-variable hypothesis ...
nfdisj1 4155 Bound-variable hypothesis ...
disjor 4156 Two ways to say that a col...
disjmoOLD 4157 Two ways to say that a col...
disjors 4158 Two ways to say that a col...
disji2 4159 Property of a disjoint col...
disji 4160 Property of a disjoint col...
invdisj 4161 If there is a function ` C...
disjiun 4162 A disjoint collection yiel...
disjiunOLD 4163 A disjoint collection yiel...
sndisj 4164 Any collection of singleto...
0disj 4165 Any collection of empty se...
disjxsn 4166 A singleton collection is ...
disjx0 4167 An empty collection is dis...
disjprg 4168 A pair collection is disjo...
disjxiun 4169 An indexed union of a disj...
disjxun 4170 The union of two disjoint ...
disjss3 4171 Expand a disjoint collecti...
breq 4174 Equality theorem for binar...
breq1 4175 Equality theorem for a bin...
breq2 4176 Equality theorem for a bin...
breq12 4177 Equality theorem for a bin...
breqi 4178 Equality inference for bin...
breq1i 4179 Equality inference for a b...
breq2i 4180 Equality inference for a b...
breq12i 4181 Equality inference for a b...
breq1d 4182 Equality deduction for a b...
breqd 4183 Equality deduction for a b...
breq2d 4184 Equality deduction for a b...
breq12d 4185 Equality deduction for a b...
breq123d 4186 Equality deduction for a b...
breqan12d 4187 Equality deduction for a b...
breqan12rd 4188 Equality deduction for a b...
nbrne1 4189 Two classes are different ...
nbrne2 4190 Two classes are different ...
eqbrtri 4191 Substitution of equal clas...
eqbrtrd 4192 Substitution of equal clas...
eqbrtrri 4193 Substitution of equal clas...
eqbrtrrd 4194 Substitution of equal clas...
breqtri 4195 Substitution of equal clas...
breqtrd 4196 Substitution of equal clas...
breqtrri 4197 Substitution of equal clas...
breqtrrd 4198 Substitution of equal clas...
3brtr3i 4199 Substitution of equality i...
3brtr4i 4200 Substitution of equality i...
3brtr3d 4201 Substitution of equality i...
3brtr4d 4202 Substitution of equality i...
3brtr3g 4203 Substitution of equality i...
3brtr4g 4204 Substitution of equality i...
syl5eqbr 4205 B chained equality inferen...
syl5eqbrr 4206 B chained equality inferen...
syl5breq 4207 B chained equality inferen...
syl5breqr 4208 B chained equality inferen...
syl6eqbr 4209 A chained equality inferen...
syl6eqbrr 4210 A chained equality inferen...
syl6breq 4211 A chained equality inferen...
syl6breqr 4212 A chained equality inferen...
ssbrd 4213 Deduction from a subclass ...
ssbri 4214 Inference from a subclass ...
nfbrd 4215 Deduction version of bound...
nfbr 4216 Bound-variable hypothesis ...
brab1 4217 Relationship between a bin...
brun 4218 The union of two binary re...
brin 4219 The intersection of two re...
brdif 4220 The difference of two bina...
sbcbrg 4221 Move substitution in and o...
sbcbr12g 4222 Move substitution in and o...
sbcbr1g 4223 Move substitution in and o...
sbcbr2g 4224 Move substitution in and o...
opabss 4229 The collection of ordered ...
opabbid 4230 Equivalent wff's yield equ...
opabbidv 4231 Equivalent wff's yield equ...
opabbii 4232 Equivalent wff's yield equ...
nfopab 4233 Bound-variable hypothesis ...
nfopab1 4234 The first abstraction vari...
nfopab2 4235 The second abstraction var...
cbvopab 4236 Rule used to change bound ...
cbvopabv 4237 Rule used to change bound ...
cbvopab1 4238 Change first bound variabl...
cbvopab2 4239 Change second bound variab...
cbvopab1s 4240 Change first bound variabl...
cbvopab1v 4241 Rule used to change the fi...
cbvopab2v 4242 Rule used to change the se...
csbopabg 4243 Move substitution into a c...
unopab 4244 Union of two ordered pair ...
mpteq12f 4245 An equality theorem for th...
mpteq12dva 4246 An equality inference for ...
mpteq12dv 4247 An equality inference for ...
mpteq12 4248 An equality theorem for th...
mpteq1 4249 An equality theorem for th...
mpteq1d 4250 An equality theorem for th...
mpteq2ia 4251 An equality inference for ...
mpteq2i 4252 An equality inference for ...
mpteq12i 4253 An equality inference for ...
mpteq2da 4254 Slightly more general equa...
mpteq2dva 4255 Slightly more general equa...
mpteq2dv 4256 An equality inference for ...
nfmpt 4257 Bound-variable hypothesis ...
nfmpt1 4258 Bound-variable hypothesis ...
cbvmpt 4259 Rule to change the bound v...
cbvmptv 4260 Rule to change the bound v...
mptv 4261 Function with universal do...
dftr2 4264 An alternate way of defini...
dftr5 4265 An alternate way of defini...
dftr3 4266 An alternate way of defini...
dftr4 4267 An alternate way of defini...
treq 4268 Equality theorem for the t...
trel 4269 In a transitive class, the...
trel3 4270 In a transitive class, the...
trss 4271 An element of a transitive...
trin 4272 The intersection of transi...
tr0 4273 The empty set is transitiv...
trv 4274 The universe is transitive...
triun 4275 The indexed union of a cla...
truni 4276 The union of a class of tr...
trint 4277 The intersection of a clas...
trintss 4278 If ` A ` is transitive and...
trint0 4279 Any non-empty transitive c...
axrep1 4281 The version of the Axiom o...
axrep2 4282 Axiom of Replacement expre...
axrep3 4283 Axiom of Replacement sligh...
axrep4 4284 A more traditional version...
axrep5 4285 Axiom of Replacement (simi...
zfrepclf 4286 An inference rule based on...
zfrep3cl 4287 An inference rule based on...
zfrep4 4288 A version of Replacement u...
axsep 4289 Separation Scheme, which i...
axsep2 4291 A less restrictive version...
zfauscl 4292 Separation Scheme (Aussond...
bm1.3ii 4293 Convert implication to equ...
ax9vsep 4294 Derive a weakened version ...
zfnuleu 4295 Show the uniqueness of the...
axnulALT 4296 Prove ~ axnul directly fro...
axnul 4297 The Null Set Axiom of ZF s...
0ex 4299 The Null Set Axiom of ZF s...
nalset 4300 No set contains all sets. ...
vprc 4301 The universal class is not...
nvel 4302 The universal class doesn'...
vnex 4303 The universal class does n...
inex1 4304 Separation Scheme (Aussond...
inex2 4305 Separation Scheme (Aussond...
inex1g 4306 Closed-form, generalized S...
ssex 4307 The subset of a set is als...
ssexi 4308 The subset of a set is als...
ssexg 4309 The subset of a set is als...
ssexd 4310 A subclass of a set is a s...
difexg 4311 Existence of a difference....
zfausab 4312 Separation Scheme (Aussond...
rabexg 4313 Separation Scheme in terms...
rabex 4314 Separation Scheme in terms...
elssabg 4315 Membership in a class abst...
intex 4316 The intersection of a non-...
intnex 4317 If a class intersection is...
intexab 4318 The intersection of a non-...
intexrab 4319 The intersection of a non-...
iinexg 4320 The existence of an indexe...
intabs 4321 Absorption of a redundant ...
inuni 4322 The intersection of a unio...
elpw2g 4323 Membership in a power clas...
elpw2 4324 Membership in a power clas...
pwnss 4325 The power set of a set is ...
pwne 4326 No set equals its power se...
class2set 4327 Construct, from any class ...
class2seteq 4328 Equality theorem based on ...
0elpw 4329 Every power class contains...
0nep0 4330 The empty set and its powe...
0inp0 4331 Something cannot be equal ...
unidif0 4332 The removal of the empty s...
iin0 4333 An indexed intersection of...
notzfaus 4334 In the Separation Scheme ~...
intv 4335 The intersection of the un...
axpweq 4336 Two equivalent ways to exp...
zfpow 4338 Axiom of Power Sets expres...
axpow2 4339 A variant of the Axiom of ...
axpow3 4340 A variant of the Axiom of ...
el 4341 Every set is an element of...
pwex 4342 Power set axiom expressed ...
pwexg 4343 Power set axiom expressed ...
abssexg 4344 Existence of a class of su...
snexALT 4345 A singleton is a set. The...
p0ex 4346 The power set of the empty...
p0exALT 4347 The power set of the empty...
pp0ex 4348 The power set of the power...
ord3ex 4349 The ordinal number 3 is a ...
dtru 4350 At least two sets exist (o...
ax16b 4351 This theorem shows that ax...
eunex 4352 Existential uniqueness imp...
nfnid 4353 A set variable is not free...
nfcvb 4354 The "distinctor" expressio...
pwuni 4355 A class is a subclass of t...
dtruALT 4356 A version of ~ dtru ("two ...
dtrucor 4357 Corollary of ~ dtru . Thi...
dtrucor2 4358 The theorem form of the de...
dvdemo1 4359 Demonstration of a theorem...
dvdemo2 4360 Demonstration of a theorem...
zfpair 4361 The Axiom of Pairing of Ze...
axpr 4362 Unabbreviated version of t...
zfpair2 4364 Derive the abbreviated ver...
snex 4365 A singleton is a set. The...
prex 4366 The Axiom of Pairing using...
elALT 4367 Every set is an element of...
dtruALT2 4368 An alternative proof of ~ ...
snelpwi 4369 A singleton of a set belon...
snelpw 4370 A singleton of a set belon...
prelpwi 4371 A pair of two sets belongs...
rext 4372 A theorem similar to exten...
sspwb 4373 Classes are subclasses if ...
unipw 4374 A class equals the union o...
pwel 4375 Membership of a power clas...
pwtr 4376 A class is transitive iff ...
ssextss 4377 An extensionality-like pri...
ssext 4378 An extensionality-like pri...
nssss 4379 Negation of subclass relat...
pweqb 4380 Classes are equal if and o...
intid 4381 The intersection of all se...
moabex 4382 "At most one" existence im...
rmorabex 4383 Restricted "at most one" e...
euabex 4384 The abstraction of a wff w...
nnullss 4385 A non-empty class (even if...
exss 4386 Restricted existence in a ...
opex 4387 An ordered pair of classes...
otex 4388 An ordered triple of class...
elop 4389 An ordered pair has two el...
opi1 4390 One of the two elements in...
opi2 4391 One of the two elements of...
opnz 4392 An ordered pair is nonempt...
opnzi 4393 An ordered pair is nonempt...
opth1 4394 Equality of the first memb...
opth 4395 The ordered pair theorem. ...
opthg 4396 Ordered pair theorem. ` C ...
opthg2 4397 Ordered pair theorem. (Co...
opth2 4398 Ordered pair theorem. (Co...
otth2 4399 Ordered triple theorem, wi...
otth 4400 Ordered triple theorem. (...
eqvinop 4401 A variable introduction la...
copsexg 4402 Substitution of class ` A ...
copsex2t 4403 Closed theorem form of ~ c...
copsex2g 4404 Implicit substitution infe...
copsex4g 4405 An implicit substitution i...
0nelop 4406 A property of ordered pair...
opeqex 4407 Equivalence of existence i...
oteqex2 4408 Equivalence of existence i...
oteqex 4409 Equivalence of existence i...
opcom 4410 An ordered pair commutes i...
moop2 4411 "At most one" property of ...
opeqsn 4412 Equivalence for an ordered...
opeqpr 4413 Equivalence for an ordered...
mosubopt 4414 "At most one" remains true...
mosubop 4415 "At most one" remains true...
euop2 4416 Transfer existential uniqu...
euotd 4417 Prove existential uniquene...
opthwiener 4418 Justification theorem for ...
uniop 4419 The union of an ordered pa...
uniopel 4420 Ordered pair membership is...
opabid 4421 The law of concretion. Sp...
elopab 4422 Membership in a class abst...
opelopabsbOLD 4423 The law of concretion in t...
brabsbOLD 4424 The law of concretion in t...
opelopabsb 4425 The law of concretion in t...
brabsb 4426 The law of concretion in t...
opelopabt 4427 Closed theorem form of ~ o...
opelopabga 4428 The law of concretion. Th...
brabga 4429 The law of concretion for ...
opelopab2a 4430 Ordered pair membership in...
opelopaba 4431 The law of concretion. Th...
braba 4432 The law of concretion for ...
opelopabg 4433 The law of concretion. Th...
brabg 4434 The law of concretion for ...
opelopab2 4435 Ordered pair membership in...
opelopab 4436 The law of concretion. Th...
brab 4437 The law of concretion for ...
opelopabaf 4438 The law of concretion. Th...
opelopabf 4439 The law of concretion. Th...
ssopab2 4440 Equivalence of ordered pai...
ssopab2b 4441 Equivalence of ordered pai...
ssopab2i 4442 Inference of ordered pair ...
ssopab2dv 4443 Inference of ordered pair ...
eqopab2b 4444 Equivalence of ordered pai...
opabn0 4445 Non-empty ordered pair cla...
iunopab 4446 Move indexed union inside ...
pwin 4447 The power class of the int...
pwunss 4448 The power class of the uni...
pwssun 4449 The power class of the uni...
pwundif 4450 Break up the power class o...
pwun 4451 The power class of the uni...
epelg 4455 The epsilon relation and m...
epelc 4456 The epsilon relationship a...
epel 4457 The epsilon relation and t...
dfid3 4459 A stronger version of ~ df...
dfid2 4460 Alternate definition of th...
poss 4465 Subset theorem for the par...
poeq1 4466 Equality theorem for parti...
poeq2 4467 Equality theorem for parti...
nfpo 4468 Bound-variable hypothesis ...
nfso 4469 Bound-variable hypothesis ...
pocl 4470 Properties of partial orde...
ispod 4471 Sufficient conditions for ...
swopolem 4472 Perform the substitutions ...
swopo 4473 A strict weak order is a p...
poirr 4474 A partial order relation i...
potr 4475 A partial order relation i...
po2nr 4476 A partial order relation h...
po3nr 4477 A partial order relation h...
po0 4478 Any relation is a partial ...
pofun 4479 A function preserves a par...
sopo 4480 A strict linear order is a...
soss 4481 Subset theorem for the str...
soeq1 4482 Equality theorem for the s...
soeq2 4483 Equality theorem for the s...
sonr 4484 A strict order relation is...
sotr 4485 A strict order relation is...
solin 4486 A strict order relation is...
so2nr 4487 A strict order relation ha...
so3nr 4488 A strict order relation ha...
sotric 4489 A strict order relation sa...
sotrieq 4490 Trichotomy law for strict ...
sotrieq2 4491 Trichotomy law for strict ...
sotr2 4492 A transitivity relation. ...
issod 4493 An irreflexive, transitive...
issoi 4494 An irreflexive, transitive...
isso2i 4495 Deduce strict ordering fro...
so0 4496 Any relation is a strict o...
somo 4497 A totally ordered set has ...
fri 4504 Property of well-founded r...
seex 4505 The ` R ` -preimage of an ...
exse 4506 Any relation on a set is s...
dffr2 4507 Alternate definition of we...
frc 4508 Property of well-founded r...
frss 4509 Subset theorem for the wel...
sess1 4510 Subset theorem for the set...
sess2 4511 Subset theorem for the set...
freq1 4512 Equality theorem for the w...
freq2 4513 Equality theorem for the w...
seeq1 4514 Equality theorem for the s...
seeq2 4515 Equality theorem for the s...
nffr 4516 Bound-variable hypothesis ...
nfse 4517 Bound-variable hypothesis ...
nfwe 4518 Bound-variable hypothesis ...
frirr 4519 A well-founded relation is...
fr2nr 4520 A well-founded relation ha...
fr0 4521 Any relation is well-found...
frminex 4522 If an element of a well-fo...
efrirr 4523 Irreflexivity of the epsil...
efrn2lp 4524 A set founded by epsilon c...
epse 4525 The epsilon relation is se...
tz7.2 4526 Similar to Theorem 7.2 of ...
dfepfr 4527 An alternate way of saying...
epfrc 4528 A subset of an epsilon-fou...
wess 4529 Subset theorem for the wel...
weeq1 4530 Equality theorem for the w...
weeq2 4531 Equality theorem for the w...
wefr 4532 A well-ordering is well-fo...
weso 4533 A well-ordering is a stric...
wecmpep 4534 The elements of an epsilon...
wetrep 4535 An epsilon well-ordering i...
wefrc 4536 A non-empty (possibly prop...
we0 4537 Any relation is a well-ord...
wereu 4538 A subset of a well-ordered...
wereu2 4539 All nonempty (possibly pro...
ordeq 4548 Equality theorem for the o...
elong 4549 An ordinal number is an or...
elon 4550 An ordinal number is an or...
eloni 4551 An ordinal number has the ...
elon2 4552 An ordinal number is an or...
limeq 4553 Equality theorem for the l...
ordwe 4554 Epsilon well-orders every ...
ordtr 4555 An ordinal class is transi...
ordfr 4556 Epsilon is well-founded on...
ordelss 4557 An element of an ordinal c...
trssord 4558 A transitive subclass of a...
ordirr 4559 Epsilon irreflexivity of o...
nordeq 4560 A member of an ordinal cla...
ordn2lp 4561 An ordinal class cannot an...
tz7.5 4562 A subclass (possibly prope...
ordelord 4563 An element of an ordinal c...
tron 4564 The class of all ordinal n...
ordelon 4565 An element of an ordinal c...
onelon 4566 An element of an ordinal n...
tz7.7 4567 Proposition 7.7 of [Takeut...
ordelssne 4568 Corollary 7.8 of [TakeutiZ...
ordelpss 4569 Corollary 7.8 of [TakeutiZ...
ordsseleq 4570 For ordinal classes, subcl...
ordin 4571 The intersection of two or...
onin 4572 The intersection of two or...
ordtri3or 4573 A trichotomy law for ordin...
ordtri1 4574 A trichotomy law for ordin...
ontri1 4575 A trichotomy law for ordin...
ordtri2 4576 A trichotomy law for ordin...
ordtri3 4577 A trichotomy law for ordin...
ordtri4 4578 A trichotomy law for ordin...
orddisj 4579 An ordinal class and its s...
onfr 4580 The ordinal class is well-...
onelpss 4581 Relationship between membe...
onsseleq 4582 Relationship between subse...
onelss 4583 An element of an ordinal n...
ordtr1 4584 Transitive law for ordinal...
ordtr2 4585 Transitive law for ordinal...
ordtr3 4586 Transitive law for ordinal...
ontr1 4587 Transitive law for ordinal...
ontr2 4588 Transitive law for ordinal...
ordunidif 4589 The union of an ordinal st...
ordintdif 4590 If ` B ` is smaller than `...
onintss 4591 If a property is true for ...
oneqmini 4592 A way to show that an ordi...
ord0 4593 The empty set is an ordina...
0elon 4594 The empty set is an ordina...
ord0eln0 4595 A non-empty ordinal contai...
on0eln0 4596 An ordinal number contains...
dflim2 4597 An alternate definition of...
inton 4598 The intersection of the cl...
nlim0 4599 The empty set is not a lim...
limord 4600 A limit ordinal is ordinal...
limuni 4601 A limit ordinal is its own...
limuni2 4602 The union of a limit ordin...
0ellim 4603 A limit ordinal contains t...
limelon 4604 A limit ordinal class that...
onn0 4605 The class of all ordinal n...
suceq 4606 Equality of successors. (...
elsuci 4607 Membership in a successor....
elsucg 4608 Membership in a successor....
elsuc2g 4609 Variant of membership in a...
elsuc 4610 Membership in a successor....
elsuc2 4611 Membership in a successor....
nfsuc 4612 Bound-variable hypothesis ...
elelsuc 4613 Membership in a successor....
sucel 4614 Membership of a successor ...
suc0 4615 The successor of the empty...
sucprc 4616 A proper class is its own ...
unisuc 4617 A transitive class is equa...
sssucid 4618 A class is included in its...
sucidg 4619 Part of Proposition 7.23 o...
sucid 4620 A set belongs to its succe...
nsuceq0 4621 No successor is empty. (C...
eqelsuc 4622 A set belongs to the succe...
iunsuc 4623 Inductive definition for t...
suctr 4624 The successor of a transti...
trsuc 4625 A set whose successor belo...
trsucss 4626 A member of the successor ...
ordsssuc 4627 A subset of an ordinal bel...
onsssuc 4628 A subset of an ordinal num...
ordsssuc2 4629 An ordinal subset of an or...
onmindif 4630 When its successor is subt...
ordnbtwn 4631 There is no set between an...
onnbtwn 4632 There is no set between an...
sucssel 4633 A set whose successor is a...
orddif 4634 Ordinal derived from its s...
orduniss 4635 An ordinal class includes ...
ordtri2or 4636 A trichotomy law for ordin...
ordtri2or2 4637 A trichotomy law for ordin...
ordtri2or3 4638 A consequence of total ord...
ordelinel 4639 The intersection of two or...
ordssun 4640 Property of a subclass of ...
ordequn 4641 The maximum (i.e. union) o...
ordun 4642 The maximum (i.e. union) o...
ordunisssuc 4643 A subclass relationship fo...
suc11 4644 The successor operation be...
onordi 4645 An ordinal number is an or...
ontrci 4646 An ordinal number is a tra...
onirri 4647 An ordinal number is not a...
oneli 4648 A member of an ordinal num...
onelssi 4649 A member of an ordinal num...
onssneli 4650 An ordering law for ordina...
onssnel2i 4651 An ordering law for ordina...
onelini 4652 An element of an ordinal n...
oneluni 4653 An ordinal number equals i...
onunisuci 4654 An ordinal number is equal...
onsseli 4655 Subset is equivalent to me...
onun2i 4656 The union of two ordinal n...
unizlim 4657 An ordinal equal to its ow...
on0eqel 4658 An ordinal number either e...
snsn0non 4659 The singleton of the singl...
zfun 4661 Axiom of Union expressed w...
axun2 4662 A variant of the Axiom of ...
uniex2 4663 The Axiom of Union using t...
uniex 4664 The Axiom of Union in clas...
uniexg 4665 The ZF Axiom of Union in c...
unex 4666 The union of two sets is a...
tpex 4667 A triple of classes exists...
unexb 4668 Existence of union is equi...
unexg 4669 A union of two sets is a s...
unisn2 4670 A version of ~ unisn witho...
unisn3 4671 Union of a singleton in th...
snnex 4672 The class of all singleton...
difex2 4673 If the subtrahend of a cla...
opeluu 4674 Each member of an ordered ...
uniuni 4675 Expression for double unio...
eusv1 4676 Two ways to express single...
eusvnf 4677 Even if ` x ` is free in `...
eusvnfb 4678 Two ways to say that ` A (...
eusv2i 4679 Two ways to express single...
eusv2nf 4680 Two ways to express single...
eusv2 4681 Two ways to express single...
reusv1 4682 Two ways to express single...
reusv2lem1 4683 Lemma for ~ reusv2 . (Con...
reusv2lem2 4684 Lemma for ~ reusv2 . (Con...
reusv2lem3 4685 Lemma for ~ reusv2 . (Con...
reusv2lem4 4686 Lemma for ~ reusv2 . (Con...
reusv2lem5 4687 Lemma for ~ reusv2 . (Con...
reusv2 4688 Two ways to express single...
reusv3i 4689 Two ways of expressing exi...
reusv3 4690 Two ways to express single...
eusv4 4691 Two ways to express single...
reusv5OLD 4692 Two ways to express single...
reusv6OLD 4693 Two ways to express single...
reusv7OLD 4694 Two ways to express single...
alxfr 4695 Transfer universal quantif...
ralxfrd 4696 Transfer universal quantif...
rexxfrd 4697 Transfer universal quantif...
ralxfr2d 4698 Transfer universal quantif...
rexxfr2d 4699 Transfer universal quantif...
ralxfr 4700 Transfer universal quantif...
ralxfrALT 4701 Transfer universal quantif...
rexxfr 4702 Transfer existence from a ...
rabxfrd 4703 Class builder membership a...
rabxfr 4704 Class builder membership a...
reuxfr2d 4705 Transfer existential uniqu...
reuxfr2 4706 Transfer existential uniqu...
reuxfrd 4707 Transfer existential uniqu...
reuxfr 4708 Transfer existential uniqu...
reuhypd 4709 A theorem useful for elimi...
reuhyp 4710 A theorem useful for elimi...
uniexb 4711 The Axiom of Union and its...
pwexb 4712 The Axiom of Power Sets an...
univ 4713 The union of the universe ...
eldifpw 4714 Membership in a power clas...
elpwun 4715 Membership in the power cl...
elpwunsn 4716 Membership in an extension...
op1stb 4717 Extract the first member o...
iunpw 4718 An indexed union of a powe...
fr3nr 4719 A well-founded relation ha...
epne3 4720 A set well-founded by epsi...
dfwe2 4721 Alternate definition of we...
ordon 4722 The class of all ordinal n...
epweon 4723 The epsilon relation well-...
onprc 4724 No set contains all ordina...
ssorduni 4725 The union of a class of or...
ssonuni 4726 The union of a set of ordi...
ssonunii 4727 The union of a set of ordi...
ordeleqon 4728 A way to express the ordin...
ordsson 4729 Any ordinal class is a sub...
onss 4730 An ordinal number is a sub...
ssonprc 4731 Two ways of saying a class...
onuni 4732 The union of an ordinal nu...
orduni 4733 The union of an ordinal cl...
onint 4734 The intersection (infimum)...
onint0 4735 The intersection of a clas...
onssmin 4736 A non-empty class of ordin...
onminesb 4737 If a property is true for ...
onminsb 4738 If a property is true for ...
oninton 4739 The intersection of a non-...
onintrab 4740 The intersection of a clas...
onintrab2 4741 An existence condition equ...
onnmin 4742 No member of a set of ordi...
onnminsb 4743 An ordinal number smaller ...
oneqmin 4744 A way to show that an ordi...
bm2.5ii 4745 Problem 2.5(ii) of [BellMa...
onminex 4746 If a wff is true for an or...
sucon 4747 The class of all ordinal n...
sucexb 4748 A successor exists iff its...
sucexg 4749 The successor of a set is ...
sucex 4750 The successor of a set is ...
onmindif2 4751 The minimum of a class of ...
suceloni 4752 The successor of an ordina...
ordsuc 4753 The successor of an ordina...
ordpwsuc 4754 The collection of ordinals...
onpwsuc 4755 The collection of ordinal ...
sucelon 4756 The successor of an ordina...
ordsucss 4757 The successor of an elemen...
onpsssuc 4758 An ordinal number is a pro...
ordelsuc 4759 A set belongs to an ordina...
onsucmin 4760 The successor of an ordina...
ordsucelsuc 4761 Membership is inherited by...
ordsucsssuc 4762 The subclass relationship ...
ordsucuniel 4763 Given an element ` A ` of ...
ordsucun 4764 The successor of the maxim...
ordunpr 4765 The maximum of two ordinal...
ordunel 4766 The maximum of two ordinal...
onsucuni 4767 A class of ordinal numbers...
ordsucuni 4768 An ordinal class is a subc...
orduniorsuc 4769 An ordinal class is either...
unon 4770 The class of all ordinal n...
ordunisuc 4771 An ordinal class is equal ...
orduniss2 4772 The union of the ordinal s...
onsucuni2 4773 A successor ordinal is the...
0elsuc 4774 The successor of an ordina...
limon 4775 The class of ordinal numbe...
onssi 4776 An ordinal number is a sub...
onsuci 4777 The successor of an ordina...
onuniorsuci 4778 An ordinal number is eithe...
onuninsuci 4779 A limit ordinal is not a s...
onsucssi 4780 A set belongs to an ordina...
nlimsucg 4781 A successor is not a limit...
orduninsuc 4782 An ordinal equal to its un...
ordunisuc2 4783 An ordinal equal to its un...
ordzsl 4784 An ordinal is zero, a succ...
onzsl 4785 An ordinal number is zero,...
dflim3 4786 An alternate definition of...
dflim4 4787 An alternate definition of...
limsuc 4788 The successor of a member ...
limsssuc 4789 A class includes a limit o...
nlimon 4790 Two ways to express the cl...
limuni3 4791 The union of a nonempty cl...
tfi 4792 The Principle of Transfini...
tfis 4793 Transfinite Induction Sche...
tfis2f 4794 Transfinite Induction Sche...
tfis2 4795 Transfinite Induction Sche...
tfis3 4796 Transfinite Induction Sche...
tfisi 4797 A transfinite induction sc...
tfinds 4798 Principle of Transfinite I...
tfindsg 4799 Transfinite Induction (inf...
tfindsg2 4800 Transfinite Induction (inf...
tfindes 4801 Transfinite Induction with...
tfinds2 4802 Transfinite Induction (inf...
tfinds3 4803 Principle of Transfinite I...
dfom2 4806 An alternate definition of...
elom 4807 Membership in omega. The ...
omsson 4808 Omega is a subset of ` On ...
limomss 4809 The class of natural numbe...
nnon 4810 A natural number is an ord...
nnoni 4811 A natural number is an ord...
nnord 4812 A natural number is ordina...
ordom 4813 Omega is ordinal. Theorem...
elnn 4814 A member of a natural numb...
omon 4815 The class of natural numbe...
omelon2 4816 Omega is an ordinal number...
nnlim 4817 A natural number is not a ...
omssnlim 4818 The class of natural numbe...
limom 4819 Omega is a limit ordinal. ...
peano2b 4820 A class belongs to omega i...
nnsuc 4821 A nonzero natural number i...
ssnlim 4822 An ordinal subclass of non...
peano1 4823 Zero is a natural number. ...
peano2 4824 The successor of any natur...
peano3 4825 The successor of any natur...
peano4 4826 Two natural numbers are eq...
peano5 4827 The induction postulate: a...
nn0suc 4828 A natural number is either...
find 4829 The Principle of Finite In...
finds 4830 Principle of Finite Induct...
findsg 4831 Principle of Finite Induct...
finds2 4832 Principle of Finite Induct...
finds1 4833 Principle of Finite Induct...
findes 4834 Finite induction with expl...
xpeq1 4851 Equality theorem for cross...
xpeq2 4852 Equality theorem for cross...
elxpi 4853 Membership in a cross prod...
elxp 4854 Membership in a cross prod...
elxp2 4855 Membership in a cross prod...
xpeq12 4856 Equality theorem for cross...
xpeq1i 4857 Equality inference for cro...
xpeq2i 4858 Equality inference for cro...
xpeq12i 4859 Equality inference for cro...
xpeq1d 4860 Equality deduction for cro...
xpeq2d 4861 Equality deduction for cro...
xpeq12d 4862 Equality deduction for cro...
nfxp 4863 Bound-variable hypothesis ...
csbxpg 4864 Distribute proper substitu...
0nelxp 4865 The empty set is not a mem...
0nelelxp 4866 A member of a cross produc...
opelxp 4867 Ordered pair membership in...
brxp 4868 Binary relation on a cross...
opelxpi 4869 Ordered pair membership in...
opelxp1 4870 The first member of an ord...
opelxp2 4871 The second member of an or...
otelxp1 4872 The first member of an ord...
rabxp 4873 Membership in a class buil...
brrelex12 4874 A true binary relation on ...
brrelex 4875 A true binary relation on ...
brrelex2 4876 A true binary relation on ...
brrelexi 4877 The first argument of a bi...
brrelex2i 4878 The second argument of a b...
nprrel 4879 No proper class is related...
fconstmpt 4880 Representation of a consta...
vtoclr 4881 Variable to class conversi...
opelvvg 4882 Ordered pair membership in...
opelvv 4883 Ordered pair membership in...
opthprc 4884 Justification theorem for ...
brel 4885 Two things in a binary rel...
brab2a 4886 Ordered pair membership in...
elxp3 4887 Membership in a cross prod...
opeliunxp 4888 Membership in a union of c...
xpundi 4889 Distributive law for cross...
xpundir 4890 Distributive law for cross...
xpiundi 4891 Distributive law for cross...
xpiundir 4892 Distributive law for cross...
iunxpconst 4893 Membership in a union of c...
xpun 4894 The cross product of two u...
elvv 4895 Membership in universal cl...
elvvv 4896 Membership in universal cl...
elvvuni 4897 An ordered pair contains i...
brinxp2 4898 Intersection of binary rel...
brinxp 4899 Intersection of binary rel...
poinxp 4900 Intersection of partial or...
soinxp 4901 Intersection of total orde...
frinxp 4902 Intersection of well-found...
seinxp 4903 Intersection of set-like r...
weinxp 4904 Intersection of well-order...
posn 4905 Partial ordering of a sing...
sosn 4906 Strict ordering on a singl...
frsn 4907 Founded relation on a sing...
wesn 4908 Well-ordering of a singlet...
opabssxp 4909 An abstraction relation is...
brab2ga 4910 The law of concretion for ...
optocl 4911 Implicit substitution of c...
2optocl 4912 Implicit substitution of c...
3optocl 4913 Implicit substitution of c...
opbrop 4914 Ordered pair membership in...
xp0r 4915 The cross product with the...
onxpdisj 4916 Ordinal numbers and ordere...
onnev 4917 The class of ordinal numbe...
releq 4918 Equality theorem for the r...
releqi 4919 Equality inference for the...
releqd 4920 Equality deduction for the...
nfrel 4921 Bound-variable hypothesis ...
relss 4922 Subclass theorem for relat...
ssrel 4923 A subclass relationship de...
eqrel 4924 Extensionality principle f...
ssrel2 4925 A subclass relationship de...
relssi 4926 Inference from subclass pr...
relssdv 4927 Deduction from subclass pr...
eqrelriv 4928 Inference from extensional...
eqrelriiv 4929 Inference from extensional...
eqbrriv 4930 Inference from extensional...
eqrelrdv 4931 Deduce equality of relatio...
eqbrrdv 4932 Deduction from extensional...
eqbrrdiv 4933 Deduction from extensional...
eqrelrdv2 4934 A version of ~ eqrelrdv . ...
ssrelrel 4935 A subclass relationship de...
eqrelrel 4936 Extensionality principle f...
elrel 4937 A member of a relation is ...
relsn 4938 A singleton is a relation ...
relsnop 4939 A singleton of an ordered ...
xpss12 4940 Subset theorem for cross p...
xpss 4941 A cross product is include...
relxp 4942 A cross product is a relat...
xpss1 4943 Subset relation for cross ...
xpss2 4944 Subset relation for cross ...
xpsspw 4945 A cross product is include...
xpsspwOLD 4946 A cross product is include...
unixpss 4947 The double class union of ...
xpexg 4948 The cross product of two s...
xpex 4949 The cross product of two s...
relun 4950 The union of two relations...
relin1 4951 The intersection with a re...
relin2 4952 The intersection with a re...
reldif 4953 A difference cutting down ...
reliun 4954 An indexed union is a rela...
reliin 4955 An indexed intersection is...
reluni 4956 The union of a class is a ...
relint 4957 The intersection of a clas...
rel0 4958 The empty set is a relatio...
relopabi 4959 A class of ordered pairs i...
relopab 4960 A class of ordered pairs i...
reli 4961 The identity relation is a...
rele 4962 The membership relation is...
opabid2 4963 A relation expressed as an...
inopab 4964 Intersection of two ordere...
difopab 4965 The difference of two orde...
inxp 4966 The intersection of two cr...
xpindi 4967 Distributive law for cross...
xpindir 4968 Distributive law for cross...
xpiindi 4969 Distributive law for cross...
xpriindi 4970 Distributive law for cross...
eliunxp 4971 Membership in a union of c...
opeliunxp2 4972 Membership in a union of c...
raliunxp 4973 Write a double restricted ...
rexiunxp 4974 Write a double restricted ...
ralxp 4975 Universal quantification r...
rexxp 4976 Existential quantification...
djussxp 4977 Disjoint union is a subset...
ralxpf 4978 Version of ~ ralxp with bo...
rexxpf 4979 Version of ~ rexxp with bo...
iunxpf 4980 Indexed union on a cross p...
opabbi2dv 4981 Deduce equality of a relat...
relop 4982 A necessary and sufficient...
ideqg 4983 For sets, the identity rel...
ideq 4984 For sets, the identity rel...
ididg 4985 A set is identical to itse...
issetid 4986 Two ways of expressing set...
coss1 4987 Subclass theorem for compo...
coss2 4988 Subclass theorem for compo...
coeq1 4989 Equality theorem for compo...
coeq2 4990 Equality theorem for compo...
coeq1i 4991 Equality inference for com...
coeq2i 4992 Equality inference for com...
coeq1d 4993 Equality deduction for com...
coeq2d 4994 Equality deduction for com...
coeq12i 4995 Equality inference for com...
coeq12d 4996 Equality deduction for com...
nfco 4997 Bound-variable hypothesis ...
brcog 4998 Ordered pair membership in...
opelco2g 4999 Ordered pair membership in...
brcogw 5000 Ordered pair membership in...
eqbrrdva 5001 Deduction from extensional...
brco 5002 Binary relation on a compo...
opelco 5003 Ordered pair membership in...
cnvss 5004 Subset theorem for convers...
cnveq 5005 Equality theorem for conve...
cnveqi 5006 Equality inference for con...
cnveqd 5007 Equality deduction for con...
elcnv 5008 Membership in a converse. ...
elcnv2 5009 Membership in a converse. ...
nfcnv 5010 Bound-variable hypothesis ...
opelcnvg 5011 Ordered-pair membership in...
brcnvg 5012 The converse of a binary r...
opelcnv 5013 Ordered-pair membership in...
brcnv 5014 The converse of a binary r...
cnvco 5015 Distributive law of conver...
cnvuni 5016 The converse of a class un...
dfdm3 5017 Alternate definition of do...
dfrn2 5018 Alternate definition of ra...
dfrn3 5019 Alternate definition of ra...
elrn2g 5020 Membership in a range. (C...
elrng 5021 Membership in a range. (C...
dfdm4 5022 Alternate definition of do...
dfdmf 5023 Definition of domain, usin...
eldmg 5024 Domain membership. Theore...
eldm2g 5025 Domain membership. Theore...
eldm 5026 Membership in a domain. T...
eldm2 5027 Membership in a domain. T...
dmss 5028 Subset theorem for domain....
dmeq 5029 Equality theorem for domai...
dmeqi 5030 Equality inference for dom...
dmeqd 5031 Equality deduction for dom...
opeldm 5032 Membership of first of an ...
breldm 5033 Membership of first of a b...
breldmg 5034 Membership of first of a b...
dmun 5035 The domain of a union is t...
dmin 5036 The domain of an intersect...
dmiun 5037 The domain of an indexed u...
dmuni 5038 The domain of a union. Pa...
dmopab 5039 The domain of a class of o...
dmopabss 5040 Upper bound for the domain...
dmopab3 5041 The domain of a restricted...
dm0 5042 The domain of the empty se...
dmi 5043 The domain of the identity...
dmv 5044 The domain of the universe...
dm0rn0 5045 An empty domain implies an...
reldm0 5046 A relation is empty iff it...
dmxp 5047 The domain of a cross prod...
dmxpid 5048 The domain of a square cro...
dmxpin 5049 The domain of the intersec...
xpid11 5050 The cross product of a cla...
dmcnvcnv 5051 The domain of the double c...
rncnvcnv 5052 The range of the double co...
elreldm 5053 The first member of an ord...
rneq 5054 Equality theorem for range...
rneqi 5055 Equality inference for ran...
rneqd 5056 Equality deduction for ran...
rnss 5057 Subset theorem for range. ...
brelrng 5058 The second argument of a b...
brelrn 5059 The second argument of a b...
opelrn 5060 Membership of second membe...
releldm 5061 The first argument of a bi...
relelrn 5062 The second argument of a b...
releldmb 5063 Membership in a domain. (...
relelrnb 5064 Membership in a range. (C...
releldmi 5065 The first argument of a bi...
relelrni 5066 The second argument of a b...
dfrnf 5067 Definition of range, using...
elrn2 5068 Membership in a range. (C...
elrn 5069 Membership in a range. (C...
nfdm 5070 Bound-variable hypothesis ...
nfrn 5071 Bound-variable hypothesis ...
dmiin 5072 Domain of an intersection....
csbrng 5073 Distribute proper substitu...
rnopab 5074 The range of a class of or...
rnmpt 5075 The range of a function in...
elrnmpt 5076 The range of a function in...
elrnmpt1s 5077 Elementhood in an image se...
elrnmpt1 5078 Elementhood in an image se...
elrnmptg 5079 Membership in the range of...
elrnmpti 5080 Membership in the range of...
dfiun3g 5081 Alternate definition of in...
dfiin3g 5082 Alternate definition of in...
dfiun3 5083 Alternate definition of in...
dfiin3 5084 Alternate definition of in...
riinint 5085 Express a relative indexed...
rn0 5086 The range of the empty set...
relrn0 5087 A relation is empty iff it...
dmrnssfld 5088 The domain and range of a ...
dmexg 5089 The domain of a set is a s...
rnexg 5090 The range of a set is a se...
dmex 5091 The domain of a set is a s...
rnex 5092 The range of a set is a se...
iprc 5093 The identity function is a...
dmcoss 5094 Domain of a composition. ...
rncoss 5095 Range of a composition. (...
dmcosseq 5096 Domain of a composition. ...
dmcoeq 5097 Domain of a composition. ...
rncoeq 5098 Range of a composition. (...
reseq1 5099 Equality theorem for restr...
reseq2 5100 Equality theorem for restr...
reseq1i 5101 Equality inference for res...
reseq2i 5102 Equality inference for res...
reseq12i 5103 Equality inference for res...
reseq1d 5104 Equality deduction for res...
reseq2d 5105 Equality deduction for res...
reseq12d 5106 Equality deduction for res...
nfres 5107 Bound-variable hypothesis ...
csbresg 5108 Distribute proper substitu...
res0 5109 A restriction to the empty...
opelres 5110 Ordered pair membership in...
brres 5111 Binary relation on a restr...
opelresg 5112 Ordered pair membership in...
brresg 5113 Binary relation on a restr...
opres 5114 Ordered pair membership in...
resieq 5115 A restricted identity rela...
opelresiOLD 5116 ` <. A , A >. ` belongs to...
opelresi 5117 ` <. A , A >. ` belongs to...
resres 5118 The restriction of a restr...
resundi 5119 Distributive law for restr...
resundir 5120 Distributive law for restr...
resindi 5121 Class restriction distribu...
resindir 5122 Class restriction distribu...
inres 5123 Move intersection into cla...
resiun1 5124 Distribution of restrictio...
resiun2 5125 Distribution of restrictio...
dmres 5126 The domain of a restrictio...
ssdmres 5127 A domain restricted to a s...
dmresexg 5128 The domain of a restrictio...
resss 5129 A class includes its restr...
rescom 5130 Commutative law for restri...
ssres 5131 Subclass theorem for restr...
ssres2 5132 Subclass theorem for restr...
relres 5133 A restriction is a relatio...
resabs1 5134 Absorption law for restric...
resabs2 5135 Absorption law for restric...
residm 5136 Idempotent law for restric...
resima 5137 A restriction to an image....
resima2 5138 Image under a restricted c...
xpssres 5139 Restriction of a constant ...
elres 5140 Membership in a restrictio...
elsnres 5141 Memebership in restriction...
relssres 5142 Simplification law for res...
resdm 5143 A relation restricted to i...
resexg 5144 The restriction of a set i...
resex 5145 The restriction of a set i...
resopab 5146 Restriction of a class abs...
resiexg 5147 The existence of a restric...
iss 5148 A subclass of the identity...
resopab2 5149 Restriction of a class abs...
resmpt 5150 Restriction of the mapping...
resmpt3 5151 Unconditional restriction ...
dfres2 5152 Alternate definition of th...
opabresid 5153 The restricted identity ex...
mptresid 5154 The restricted identity ex...
dmresi 5155 The domain of a restricted...
resid 5156 Any relation restricted to...
imaeq1 5157 Equality theorem for image...
imaeq2 5158 Equality theorem for image...
imaeq1i 5159 Equality theorem for image...
imaeq2i 5160 Equality theorem for image...
imaeq1d 5161 Equality theorem for image...
imaeq2d 5162 Equality theorem for image...
imaeq12d 5163 Equality theorem for image...
dfima2 5164 Alternate definition of im...
dfima3 5165 Alternate definition of im...
elimag 5166 Membership in an image. T...
elima 5167 Membership in an image. T...
elima2 5168 Membership in an image. T...
elima3 5169 Membership in an image. T...
nfima 5170 Bound-variable hypothesis ...
nfimad 5171 Deduction version of bound...
csbima12g 5172 Move class substitution in...
csbima12gALT 5173 Move class substitution in...
imadmrn 5174 The image of the domain of...
imassrn 5175 The image of a class is a ...
imaexg 5176 The image of a set is a se...
imai 5177 Image under the identity r...
rnresi 5178 The range of the restricte...
resiima 5179 The image of a restriction...
ima0 5180 Image of the empty set. T...
0ima 5181 Image under the empty rela...
imadisj 5182 A class whose image under ...
cnvimass 5183 A preimage under any class...
cnvimarndm 5184 The preimage of the range ...
imasng 5185 The image of a singleton. ...
relimasn 5186 The image of a singleton. ...
elrelimasn 5187 Elementhood in the image o...
elimasn 5188 Membership in an image of ...
elimasng 5189 Membership in an image of ...
elimasni 5190 Membership in an image of ...
args 5191 Two ways to express the cl...
eliniseg 5192 Membership in an initial s...
epini 5193 Any set is equal to its pr...
iniseg 5194 An idiom that signifies an...
dffr3 5195 Alternate definition of we...
dfse2 5196 Alternate definition of se...
exse2 5197 Any set relation is set-li...
imass1 5198 Subset theorem for image. ...
imass2 5199 Subset theorem for image. ...
ndmima 5200 The image of a singleton o...
relcnv 5201 A converse is a relation. ...
relbrcnvg 5202 When ` R ` is a relation, ...
eliniseg2 5203 Eliminate the class existe...
relbrcnv 5204 When ` R ` is a relation, ...
cotr 5205 Two ways of saying a relat...
issref 5206 Two ways to state a relati...
cnvsym 5207 Two ways of saying a relat...
intasym 5208 Two ways of saying a relat...
asymref 5209 Two ways of saying a relat...
asymref2 5210 Two ways of saying a relat...
intirr 5211 Two ways of saying a relat...
brcodir 5212 Two ways of saying that tw...
codir 5213 Two ways of saying a relat...
qfto 5214 A quantifier-free way of e...
xpidtr 5215 A square cross product ` (...
trin2 5216 The intersection of two tr...
poirr2 5217 A partial order relation i...
trinxp 5218 The relation induced by a ...
soirri 5219 A strict order relation is...
sotri 5220 A strict order relation is...
son2lpi 5221 A strict order relation ha...
sotri2 5222 A transitivity relation. ...
sotri3 5223 A transitivity relation. ...
soirriOLD 5224 A strict order relation is...
sotriOLD 5225 A strict order relation is...
son2lpiOLD 5226 A strict order relation ha...
poleloe 5227 Express "less than or equa...
poltletr 5228 Transitive law for general...
somin1 5229 Property of a minimum in a...
somincom 5230 Commutativity of minimum i...
somin2 5231 Property of a minimum in a...
soltmin 5232 Being less than a minimum,...
cnvopab 5233 The converse of a class ab...
cnv0 5234 The converse of the empty ...
cnvi 5235 The converse of the identi...
cnvun 5236 The converse of a union is...
cnvdif 5237 Distributive law for conve...
cnvin 5238 Distributive law for conve...
rnun 5239 Distributive law for range...
rnin 5240 The range of an intersecti...
rniun 5241 The range of an indexed un...
rnuni 5242 The range of a union. Par...
imaundi 5243 Distributive law for image...
imaundir 5244 The image of a union. (Co...
dminss 5245 An upper bound for interse...
imainss 5246 An upper bound for interse...
inimass 5247 The image of an intersecti...
inimasn 5248 The intersection of the im...
cnvxp 5249 The converse of a cross pr...
xp0 5250 The cross product with the...
xpnz 5251 The cross product of nonem...
xpeq0 5252 At least one member of an ...
xpdisj1 5253 Cross products with disjoi...
xpdisj2 5254 Cross products with disjoi...
xpsndisj 5255 Cross products with two di...
djudisj 5256 Disjoint unions with disjo...
resdisj 5257 A double restriction to di...
rnxp 5258 The range of a cross produ...
dmxpss 5259 The domain of a cross prod...
rnxpss 5260 The range of a cross produ...
rnxpid 5261 The range of a square cros...
ssxpb 5262 A cross-product subclass r...
xp11 5263 The cross product of non-e...
xpcan 5264 Cancellation law for cross...
xpcan2 5265 Cancellation law for cross...
xpexr 5266 If a cross product is a se...
xpexr2 5267 If a nonempty cross produc...
ssrnres 5268 Subset of the range of a r...
rninxp 5269 Range of the intersection ...
dminxp 5270 Domain of the intersection...
imainrect 5271 Image of a relation restri...
xpima 5272 The image by a constant fu...
xpima1 5273 The image by a cross produ...
xpima2 5274 The image by a cross produ...
xpimasn 5275 The image of a singleton b...
sossfld 5276 The base set of a strict o...
sofld 5277 The base set of a nonempty...
soex 5278 If the relation in a stric...
cnvcnv3 5279 The set of all ordered pai...
dfrel2 5280 Alternate definition of re...
dfrel4v 5281 A relation can be expresse...
cnvcnv 5282 The double converse of a c...
cnvcnv2 5283 The double converse of a c...
cnvcnvss 5284 The double converse of a c...
cnveqb 5285 Equality theorem for conve...
cnveq0 5286 A relation empty iff its c...
dfrel3 5287 Alternate definition of re...
dmresv 5288 The domain of a universal ...
rnresv 5289 The range of a universal r...
dfrn4 5290 Range defined in terms of ...
rescnvcnv 5291 The restriction of the dou...
cnvcnvres 5292 The double converse of the...
imacnvcnv 5293 The image of the double co...
dmsnn0 5294 The domain of a singleton ...
rnsnn0 5295 The range of a singleton i...
dmsn0 5296 The domain of the singleto...
cnvsn0 5297 The converse of the single...
dmsn0el 5298 The domain of a singleton ...
relsn2 5299 A singleton is a relation ...
dmsnopg 5300 The domain of a singleton ...
dmsnopss 5301 The domain of a singleton ...
dmpropg 5302 The domain of an unordered...
dmsnop 5303 The domain of a singleton ...
dmprop 5304 The domain of an unordered...
dmtpop 5305 The domain of an unordered...
cnvcnvsn 5306 Double converse of a singl...
dmsnsnsn 5307 The domain of the singleto...
rnsnopg 5308 The range of a singleton o...
rnsnop 5309 The range of a singleton o...
op1sta 5310 Extract the first member o...
cnvsn 5311 Converse of a singleton of...
op2ndb 5312 Extract the second member ...
op2nda 5313 Extract the second member ...
cnvsng 5314 Converse of a singleton of...
opswap 5315 Swap the members of an ord...
elxp4 5316 Membership in a cross prod...
elxp5 5317 Membership in a cross prod...
cnvresima 5318 An image under the convers...
resdm2 5319 A class restricted to its ...
resdmres 5320 Restriction to the domain ...
imadmres 5321 The image of the domain of...
mptpreima 5322 The preimage of a function...
mptiniseg 5323 Converse singleton image o...
dmmpt 5324 The domain of the mapping ...
dmmptss 5325 The domain of a mapping is...
dmmptg 5326 The domain of the mapping ...
relco 5327 A composition is a relatio...
dfco2 5328 Alternate definition of a ...
dfco2a 5329 Generalization of ~ dfco2 ...
coundi 5330 Class composition distribu...
coundir 5331 Class composition distribu...
cores 5332 Restricted first member of...
resco 5333 Associative law for the re...
imaco 5334 Image of the composition o...
rnco 5335 The range of the compositi...
rnco2 5336 The range of the compositi...
dmco 5337 The domain of a compositio...
coiun 5338 Composition with an indexe...
cocnvcnv1 5339 A composition is not affec...
cocnvcnv2 5340 A composition is not affec...
cores2 5341 Absorption of a reverse (p...
co02 5342 Composition with the empty...
co01 5343 Composition with the empty...
coi1 5344 Composition with the ident...
coi2 5345 Composition with the ident...
coires1 5346 Composition with a restric...
coass 5347 Associative law for class ...
relcnvtr 5348 A relation is transitive i...
relssdmrn 5349 A relation is included in ...
cnvssrndm 5350 The converse is a subset o...
cossxp 5351 Composition as a subset of...
relrelss 5352 Two ways to describe the s...
unielrel 5353 The membership relation fo...
relfld 5354 The double union of a rela...
relresfld 5355 Restriction of a relation ...
relcoi2 5356 Composition with the ident...
relcoi1 5357 Composition with the ident...
unidmrn 5358 The double union of the co...
relcnvfld 5359 if ` R ` is a relation, it...
dfdm2 5360 Alternate definition of do...
unixp 5361 The double class union of ...
unixp0 5362 A cross product is empty i...
unixpid 5363 Field of a square cross pr...
cnvexg 5364 The converse of a set is a...
cnvex 5365 The converse of a set is a...
relcnvexb 5366 A relation is a set iff it...
ressn 5367 Restriction of a class to ...
cnviin 5368 The converse of an interse...
cnvpo 5369 The converse of a partial ...
cnvso 5370 The converse of a strict o...
coexg 5371 The composition of two set...
coex 5372 The composition of two set...
xpco 5373 Composition of two cross p...
xpcoid 5374 Composition of two square ...
iotajust 5376 Soundness justification th...
dfiota2 5378 Alternate definition for d...
nfiota1 5379 Bound-variable hypothesis ...
nfiotad 5380 Deduction version of ~ nfi...
nfiota 5381 Bound-variable hypothesis ...
cbviota 5382 Change bound variables in ...
cbviotav 5383 Change bound variables in ...
sb8iota 5384 Variable substitution in d...
iotaeq 5385 Equality theorem for descr...
iotabi 5386 Equivalence theorem for de...
uniabio 5387 Part of Theorem 8.17 in [Q...
iotaval 5388 Theorem 8.19 in [Quine] p....
iotauni 5389 Equivalence between two di...
iotaint 5390 Equivalence between two di...
iota1 5391 Property of iota. (Contri...
iotanul 5392 Theorem 8.22 in [Quine] p....
iotassuni 5393 The ` iota ` class is a su...
iotaex 5394 Theorem 8.23 in [Quine] p....
iota4 5395 Theorem *14.22 in [Whitehe...
iota4an 5396 Theorem *14.23 in [Whitehe...
iota5 5397 A method for computing iot...
iotabidv 5398 Formula-building deduction...
iotabii 5399 Formula-building deduction...
iotacl 5400 Membership law for descrip...
iota2df 5401 A condition that allows us...
iota2d 5402 A condition that allows us...
iota2 5403 The unique element such th...
sniota 5404 A class abstraction with a...
dfiota4 5405 The ` iota ` operation usi...
csbiotag 5406 Class substitution within ...
dffun2 5423 Alternate definition of a ...
dffun3 5424 Alternate definition of fu...
dffun4 5425 Alternate definition of a ...
dffun5 5426 Alternate definition of fu...
dffun6f 5427 Definition of function, us...
dffun6 5428 Alternate definition of a ...
funmo 5429 A function has at most one...
funrel 5430 A function is a relation. ...
funss 5431 Subclass theorem for funct...
funeq 5432 Equality theorem for funct...
funeqi 5433 Equality inference for the...
funeqd 5434 Equality deduction for the...
nffun 5435 Bound-variable hypothesis ...
funeu 5436 There is exactly one value...
funeu2 5437 There is exactly one value...
dffun7 5438 Alternate definition of a ...
dffun8 5439 Alternate definition of a ...
dffun9 5440 Alternate definition of a ...
funfn 5441 An equivalence for the fun...
funi 5442 The identity relation is a...
nfunv 5443 The universe is not a func...
funopg 5444 A Kuratowski ordered pair ...
funopab 5445 A class of ordered pairs i...
funopabeq 5446 A class of ordered pairs o...
funopab4 5447 A class of ordered pairs o...
funmpt 5448 A function in maps-to nota...
funmpt2 5449 Functionality of a class g...
funco 5450 The composition of two fun...
funres 5451 A restriction of a functio...
funssres 5452 The restriction of a funct...
fun2ssres 5453 Equality of restrictions o...
funun 5454 The union of functions wit...
funcnvsn 5455 The converse singleton of ...
funsng 5456 A singleton of an ordered ...
fnsng 5457 Functionality and domain o...
funsn 5458 A singleton of an ordered ...
funprg 5459 A set of two pairs is a fu...
funtpg 5460 A set of three pairs is a ...
funpr 5461 A function with a domain o...
funtp 5462 A function with a domain o...
fnsn 5463 Functionality and domain o...
fnprg 5464 Function with a domain of ...
fntpg 5465 Function with a domain of ...
fntp 5466 A function with a domain o...
fun0 5467 The empty set is a functio...
funcnvcnv 5468 The double converse of a f...
funcnv2 5469 A simpler equivalence for ...
funcnv 5470 The converse of a class is...
funcnv3 5471 A condition showing a clas...
fun2cnv 5472 The double converse of a c...
svrelfun 5473 A single-valued relation i...
fncnv 5474 Single-rootedness (see ~ f...
fun11 5475 Two ways of stating that `...
fununi 5476 The union of a chain (with...
funcnvuni 5477 The union of a chain (with...
fun11uni 5478 The union of a chain (with...
funin 5479 The intersection with a fu...
funres11 5480 The restriction of a one-t...
funcnvres 5481 The converse of a restrict...
cnvresid 5482 Converse of a restricted i...
funcnvres2 5483 The converse of a restrict...
funimacnv 5484 The image of the preimage ...
funimass1 5485 A kind of contraposition l...
funimass2 5486 A kind of contraposition l...
imadif 5487 The image of a difference ...
imain 5488 The image of an intersecti...
funimaexg 5489 Axiom of Replacement using...
funimaex 5490 The image of a set under a...
isarep1 5491 Part of a study of the Axi...
isarep2 5492 Part of a study of the Axi...
fneq1 5493 Equality theorem for funct...
fneq2 5494 Equality theorem for funct...
fneq1d 5495 Equality deduction for fun...
fneq2d 5496 Equality deduction for fun...
fneq12d 5497 Equality deduction for fun...
fneq1i 5498 Equality inference for fun...
fneq2i 5499 Equality inference for fun...
nffn 5500 Bound-variable hypothesis ...
fnfun 5501 A function with domain is ...
fnrel 5502 A function with domain is ...
fndm 5503 The domain of a function. ...
funfni 5504 Inference to convert a fun...
fndmu 5505 A function has a unique do...
fnbr 5506 The first argument of bina...
fnop 5507 The first argument of an o...
fneu 5508 There is exactly one value...
fneu2 5509 There is exactly one value...
fnun 5510 The union of two functions...
fnunsn 5511 Extension of a function wi...
fnco 5512 Composition of two functio...
fnresdm 5513 A function does not change...
fnresdisj 5514 A function restricted to a...
2elresin 5515 Membership in two function...
fnssresb 5516 Restriction of a function ...
fnssres 5517 Restriction of a function ...
fnresin1 5518 Restriction of a function'...
fnresin2 5519 Restriction of a function'...
fnres 5520 An equivalence for functio...
fnresi 5521 Functionality and domain o...
fnima 5522 The image of a function's ...
fn0 5523 A function with empty doma...
fnimadisj 5524 A class that is disjoint w...
fnimaeq0 5525 Images under a function ne...
dfmpt3 5526 Alternate definition for t...
fnopabg 5527 Functionality and domain o...
fnopab 5528 Functionality and domain o...
mptfng 5529 The maps-to notation defin...
fnmpt 5530 The maps-to notation defin...
mpt0 5531 A mapping operation with e...
fnmpti 5532 Functionality and domain o...
dmmpti 5533 Domain of an ordered-pair ...
mptun 5534 Union of mappings which ar...
feq1 5535 Equality theorem for funct...
feq2 5536 Equality theorem for funct...
feq3 5537 Equality theorem for funct...
feq23 5538 Equality theorem for funct...
feq1d 5539 Equality deduction for fun...
feq2d 5540 Equality deduction for fun...
feq12d 5541 Equality deduction for fun...
feq123d 5542 Equality deduction for fun...
feq123 5543 Equality theorem for funct...
feq1i 5544 Equality inference for fun...
feq2i 5545 Equality inference for fun...
feq23i 5546 Equality inference for fun...
feq23d 5547 Equality deduction for fun...
nff 5548 Bound-variable hypothesis ...
elimf 5549 Eliminate a mapping hypoth...
ffn 5550 A mapping is a function. ...
dffn2 5551 Any function is a mapping ...
ffun 5552 A mapping is a function. ...
frel 5553 A mapping is a relation. ...
fdm 5554 The domain of a mapping. ...
fdmi 5555 The domain of a mapping. ...
frn 5556 The range of a mapping. (...
dffn3 5557 A function maps to its ran...
fss 5558 Expanding the codomain of ...
fco 5559 Composition of two mapping...
fco2 5560 Functionality of a composi...
fssxp 5561 A mapping is a class of or...
fex2 5562 A function with bounded do...
funssxp 5563 Two ways of specifying a p...
ffdm 5564 A mapping is a partial fun...
opelf 5565 The members of an ordered ...
fun 5566 The union of two functions...
fun2 5567 The union of two functions...
fnfco 5568 Composition of two functio...
fssres 5569 Restriction of a function ...
fssres2 5570 Restriction of a restricte...
fresin 5571 An identity for the mappin...
resasplit 5572 If two functions agree on ...
fresaun 5573 The union of two functions...
fresaunres2 5574 From the union of two func...
fresaunres1 5575 From the union of two func...
fcoi1 5576 Composition of a mapping a...
fcoi2 5577 Composition of restricted ...
feu 5578 There is exactly one value...
fcnvres 5579 The converse of a restrict...
fimacnvdisj 5580 The preimage of a class di...
fint 5581 Function into an intersect...
fin 5582 Mapping into an intersecti...
fabexg 5583 Existence of a set of func...
fabex 5584 Existence of a set of func...
dmfex 5585 If a mapping is a set, its...
f0 5586 The empty function. (Cont...
f00 5587 A class is a function with...
fconst 5588 A cross product with a sin...
fconstg 5589 A cross product with a sin...
fnconstg 5590 A cross product with a sin...
fconst6g 5591 Constant function with loo...
fconst6 5592 A constant function as a m...
f1eq1 5593 Equality theorem for one-t...
f1eq2 5594 Equality theorem for one-t...
f1eq3 5595 Equality theorem for one-t...
nff1 5596 Bound-variable hypothesis ...
dff12 5597 Alternate definition of a ...
f1f 5598 A one-to-one mapping is a ...
f1fn 5599 A one-to-one mapping is a ...
f1fun 5600 A one-to-one mapping is a ...
f1rel 5601 A one-to-one onto mapping ...
f1dm 5602 The domain of a one-to-one...
f1ss 5603 A function that is one-to-...
f1ssr 5604 Combine a one-to-one funct...
f1ssres 5605 A function that is one-to-...
f1cnvcnv 5606 Two ways to express that a...
f1co 5607 Composition of one-to-one ...
foeq1 5608 Equality theorem for onto ...
foeq2 5609 Equality theorem for onto ...
foeq3 5610 Equality theorem for onto ...
nffo 5611 Bound-variable hypothesis ...
fof 5612 An onto mapping is a mappi...
fofun 5613 An onto mapping is a funct...
fofn 5614 An onto mapping is a funct...
forn 5615 The codomain of an onto fu...
dffo2 5616 Alternate definition of an...
foima 5617 The image of the domain of...
dffn4 5618 A function maps onto its r...
funforn 5619 A function maps its domain...
fodmrnu 5620 An onto function has uniqu...
fores 5621 Restriction of a function....
foco 5622 Composition of onto functi...
foconst 5623 A nonzero constant functio...
f1oeq1 5624 Equality theorem for one-t...
f1oeq2 5625 Equality theorem for one-t...
f1oeq3 5626 Equality theorem for one-t...
f1oeq23 5627 Equality theorem for one-t...
f1eq123d 5628 Equality deduction for one...
foeq123d 5629 Equality deduction for ont...
f1oeq123d 5630 Equality deduction for one...
nff1o 5631 Bound-variable hypothesis ...
f1of1 5632 A one-to-one onto mapping ...
f1of 5633 A one-to-one onto mapping ...
f1ofn 5634 A one-to-one onto mapping ...
f1ofun 5635 A one-to-one onto mapping ...
f1orel 5636 A one-to-one onto mapping ...
f1odm 5637 The domain of a one-to-one...
dff1o2 5638 Alternate definition of on...
dff1o3 5639 Alternate definition of on...
f1ofo 5640 A one-to-one onto function...
dff1o4 5641 Alternate definition of on...
dff1o5 5642 Alternate definition of on...
f1orn 5643 A one-to-one function maps...
f1f1orn 5644 A one-to-one function maps...
f1oabexg 5645 The class of all 1-1-onto ...
f1ocnv 5646 The converse of a one-to-o...
f1ocnvb 5647 A relation is a one-to-one...
f1ores 5648 The restriction of a one-t...
f1orescnv 5649 The converse of a one-to-o...
f1imacnv 5650 Preimage of an image. (Co...
foimacnv 5651 A reverse version of ~ f1i...
foun 5652 The union of two onto func...
f1oun 5653 The union of two one-to-on...
fun11iun 5654 The union of a chain (with...
resdif 5655 The restriction of a one-t...
resin 5656 The restriction of a one-t...
f1oco 5657 Composition of one-to-one ...
f1cnv 5658 The converse of an injecti...
funcocnv2 5659 Composition with the conve...
fococnv2 5660 The composition of an onto...
f1ococnv2 5661 The composition of a one-t...
f1cocnv2 5662 Composition of an injectiv...
f1ococnv1 5663 The composition of a one-t...
f1cocnv1 5664 Composition of an injectiv...
funcoeqres 5665 Re-express a constraint on...
ffoss 5666 Relationship between a map...
f11o 5667 Relationship between one-t...
f10 5668 The empty set maps one-to-...
f1o00 5669 One-to-one onto mapping of...
fo00 5670 Onto mapping of the empty ...
f1o0 5671 One-to-one onto mapping of...
f1oi 5672 A restriction of the ident...
f1ovi 5673 The identity relation is a...
f1osn 5674 A singleton of an ordered ...
f1osng 5675 A singleton of an ordered ...
f1oprswap 5676 A two-element swap is a bi...
f1oprg 5677 An unordered pair of order...
tz6.12-2 5678 Function value when ` F ` ...
fveu 5679 The value of a function at...
brprcneu 5680 If ` A ` is a proper class...
fvprc 5681 A function's value at a pr...
fv2 5682 Alternate definition of fu...
dffv3 5683 A definition of function v...
dffv4 5684 The previous definition of...
elfv 5685 Membership in a function v...
fveq1 5686 Equality theorem for funct...
fveq2 5687 Equality theorem for funct...
fveq1i 5688 Equality inference for fun...
fveq1d 5689 Equality deduction for fun...
fveq2i 5690 Equality inference for fun...
fveq2d 5691 Equality deduction for fun...
fveq12i 5692 Equality deduction for fun...
fveq12d 5693 Equality deduction for fun...
nffv 5694 Bound-variable hypothesis ...
nffvmpt1 5695 Bound-variable hypothesis ...
nffvd 5696 Deduction version of bound...
csbfv12g 5697 Move class substitution in...
csbfv12gALT 5698 Move class substitution in...
csbfv2g 5699 Move class substitution in...
csbfvg 5700 Substitution for a functio...
fvex 5701 The value of a class exist...
fvif 5702 Move a conditional outside...
fv3 5703 Alternate definition of th...
fvres 5704 The value of a restricted ...
funssfv 5705 The value of a member of t...
tz6.12-1 5706 Function value. Theorem 6...
tz6.12 5707 Function value. Theorem 6...
tz6.12f 5708 Function value, using boun...
tz6.12c 5709 Corollary of Theorem 6.12(...
tz6.12i 5710 Corollary of Theorem 6.12(...
fvbr0 5711 Two possibilities for the ...
fvrn0 5712 A function value is a memb...
fvssunirn 5713 The result of a function v...
ndmfv 5714 The value of a class outsi...
ndmfvrcl 5715 Reverse closure law for fu...
elfvdm 5716 If a function value has a ...
elfvex 5717 If a function value has a ...
elfvexd 5718 If a function value is non...
nfvres 5719 The value of a non-member ...
nfunsn 5720 If the restriction of a cl...
fvfundmfvn0 5721 If a class' value at an ar...
fv01 5722 Function value of the empt...
fveqres 5723 Equal values imply equal v...
funbrfv 5724 The second argument of a b...
funopfv 5725 The second element in an o...
fnbrfvb 5726 Equivalence of function va...
fnopfvb 5727 Equivalence of function va...
funbrfvb 5728 Equivalence of function va...
funopfvb 5729 Equivalence of function va...
funbrfv2b 5730 Function value in terms of...
dffn5 5731 Representation of a functi...
fnrnfv 5732 The range of a function ex...
fvelrnb 5733 A member of a function's r...
dfimafn 5734 Alternate definition of th...
dfimafn2 5735 Alternate definition of th...
funimass4 5736 Membership relation for th...
fvelima 5737 Function value in an image...
feqmptd 5738 Deduction form of ~ dffn5 ...
feqresmpt 5739 Express a restricted funct...
dffn5f 5740 Representation of a functi...
fvelimab 5741 Function value in an image...
fvi 5742 The value of the identity ...
fviss 5743 The value of the identity ...
fniinfv 5744 The indexed intersection o...
fnsnfv 5745 Singleton of function valu...
fnimapr 5746 The image of a pair under ...
ssimaex 5747 The existence of a subimag...
ssimaexg 5748 The existence of a subimag...
funfv 5749 A simplified expression fo...
funfv2 5750 The value of a function. ...
funfv2f 5751 The value of a function. ...
fvun 5752 Value of the union of two ...
fvun1 5753 The value of a union when ...
fvun2 5754 The value of a union when ...
dffv2 5755 Alternate definition of fu...
dmfco 5756 Domains of a function comp...
fvco2 5757 Value of a function compos...
fvco 5758 Value of a function compos...
fvco3 5759 Value of a function compos...
fvco4i 5760 Conditions for a compositi...
fvopab3g 5761 Value of a function given ...
fvopab3ig 5762 Value of a function given ...
fvmptg 5763 Value of a function given ...
fvmpti 5764 Value of a function given ...
fvmpt 5765 Value of a function given ...
fvmpts 5766 Value of a function given ...
fvmpt3 5767 Value of a function given ...
fvmpt3i 5768 Value of a function given ...
fvmptd 5769 Deduction version of ~ fvm...
fvmpt2i 5770 Value of a function given ...
fvmpt2 5771 Value of a function given ...
fvmptss 5772 If all the values of the m...
fvmpt2d 5773 Deduction version of ~ fvm...
fvmptex 5774 Express a function ` F ` w...
fvmptdf 5775 Alternate deduction versio...
fvmptdv 5776 Alternate deduction versio...
fvmptdv2 5777 Alternate deduction versio...
mpteqb 5778 Bidirectional equality the...
fvmptt 5779 Closed theorem form of ~ f...
fvmptf 5780 Value of a function given ...
fvmptnf 5781 The value of a function gi...
fvmptn 5782 This somewhat non-intuitiv...
fvmptss2 5783 A mapping always evaluates...
fvopab4ndm 5784 Value of a function given ...
fvopab6 5785 Value of a function given ...
eqfnfv 5786 Equality of functions is d...
eqfnfv2 5787 Equality of functions is d...
eqfnfv3 5788 Derive equality of functio...
eqfnfvd 5789 Deduction for equality of ...
eqfnfv2f 5790 Equality of functions is d...
eqfunfv 5791 Equality of functions is d...
fvreseq 5792 Equality of restricted fun...
fndmdif 5793 Two ways to express the lo...
fndmdifcom 5794 The difference set between...
fndmdifeq0 5795 The difference set of two ...
fndmin 5796 Two ways to express the lo...
fneqeql 5797 Two functions are equal if...
fneqeql2 5798 Two functions are equal if...
fnreseql 5799 Two functions are equal on...
chfnrn 5800 The range of a choice func...
funfvop 5801 Ordered pair with function...
funfvbrb 5802 Two ways to say that ` A `...
fvimacnvi 5803 A member of a preimage is ...
fvimacnv 5804 The argument of a function...
funimass3 5805 A kind of contraposition l...
funimass5 5806 A subclass of a preimage i...
funconstss 5807 Two ways of specifying tha...
fvimacnvALT 5808 Another proof of ~ fvimacn...
elpreima 5809 Membership in the preimage...
fniniseg 5810 Membership in the preimage...
fncnvima2 5811 Inverse images under funct...
fniniseg2 5812 Inverse point images under...
fnniniseg2 5813 Support sets of functions ...
rexsupp 5814 Existential quantification...
unpreima 5815 Preimage of a union. (Con...
inpreima 5816 Preimage of an intersectio...
difpreima 5817 Preimage of a difference. ...
respreima 5818 The preimage of a restrict...
iinpreima 5819 Preimage of an intersectio...
intpreima 5820 Preimage of an intersectio...
fimacnv 5821 The preimage of the codoma...
suppss 5822 Show that the support of a...
suppssr 5823 A function is zero outside...
fnopfv 5824 Ordered pair with function...
fvelrn 5825 A function's value belongs...
fnfvelrn 5826 A function's value belongs...
ffvelrn 5827 A function's value belongs...
ffvelrni 5828 A function's value belongs...
ffvelrnda 5829 A function's value belongs...
ffvelrnd 5830 A function's value belongs...
rexrn 5831 Restricted existential qua...
ralrn 5832 Restricted universal quant...
elrnrexdm 5833 For any element in the ran...
elrnrexdmb 5834 For any element in the ran...
eldmrexrn 5835 For any element in the dom...
eldmrexrnb 5836 For any element in the dom...
ralrnmpt 5837 A restricted quantifier ov...
rexrnmpt 5838 A restricted quantifier ov...
f0cli 5839 Unconditional closure of a...
dff2 5840 Alternate definition of a ...
dff3 5841 Alternate definition of a ...
dff4 5842 Alternate definition of a ...
dffo3 5843 An onto mapping expressed ...
dffo4 5844 Alternate definition of an...
dffo5 5845 Alternate definition of an...
exfo 5846 A relation equivalent to t...
foelrn 5847 Property of a surjective f...
foco2 5848 If a composition of two fu...
fmpt 5849 Functionality of the mappi...
f1ompt 5850 Express bijection for a ma...
fmpti 5851 Functionality of the mappi...
fmptd 5852 Domain and codomain of the...
ffnfv 5853 A function maps to a class...
ffnfvf 5854 A function maps to a class...
fnfvrnss 5855 An upper bound for range d...
rnmptss 5856 The range of an operation ...
fmpt2d 5857 Domain and codomain of the...
fmpt2dOLD 5858 Domain and codomain of the...
ffvresb 5859 A necessary and sufficient...
fmptco 5860 Composition of two functio...
fmptcof 5861 Version of ~ fmptco where ...
fmptcos 5862 Composition of two functio...
fcompt 5863 Express composition of two...
fcoconst 5864 Composition with a constan...
fsn 5865 A function maps a singleto...
fsng 5866 A function maps a singleto...
fsn2 5867 A function that maps a sin...
xpsng 5868 The cross product of two s...
xpsn 5869 The cross product of two s...
dfmpt 5870 Alternate definition for t...
fnasrn 5871 A function expressed as th...
ressnop0 5872 If ` A ` is not in ` C ` ,...
fpr 5873 A function with a domain o...
fprg 5874 A function with a domain o...
ftpg 5875 A function with a domain o...
ftp 5876 A function with a domain o...
fnressn 5877 A function restricted to a...
funressn 5878 A function restricted to a...
fressnfv 5879 The value of a function re...
fvconst 5880 The value of a constant fu...
fmptsn 5881 Express a singleton functi...
fmptap 5882 Append an additional value...
fvresi 5883 The value of a restricted ...
fvunsn 5884 Remove an ordered pair not...
fvsn 5885 The value of a singleton o...
fvsng 5886 The value of a singleton o...
fvsnun1 5887 The value of a function wi...
fvsnun2 5888 The value of a function wi...
fnsnsplit 5889 Split a function into a si...
fsnunf 5890 Adjoining a point to a fun...
fsnunf2 5891 Adjoining a point to a pun...
fsnunfv 5892 Recover the added point fr...
fsnunres 5893 Recover the original funct...
fvpr1 5894 The value of a function wi...
fvpr2 5895 The value of a function wi...
fvpr1g 5896 The value of a function wi...
fvpr2g 5897 The value of a function wi...
fvtp1 5898 The first value of a funct...
fvtp2 5899 The second value of a func...
fvtp3 5900 The third value of a funct...
fvtp1g 5901 The value of a function wi...
fvtp2g 5902 The value of a function wi...
fvtp3g 5903 The value of a function wi...
fvconst2g 5904 The value of a constant fu...
fconst2g 5905 A constant function expres...
fvconst2 5906 The value of a constant fu...
fconst2 5907 A constant function expres...
fconst5 5908 Two ways to express that a...
fnpr 5909 Representation as a set of...
fnprOLD 5910 Representation as a set of...
fnsuppres 5911 Two ways to express restri...
fnsuppeq0 5912 The support of a function ...
fconstfv 5913 A constant function expres...
fconst3 5914 Two ways to express a cons...
fconst4 5915 Two ways to express a cons...
resfunexg 5916 The restriction of a funct...
resfunexgALT 5917 The restriction of a funct...
cofunexg 5918 Existence of a composition...
cofunex2g 5919 Existence of a composition...
fnex 5920 If the domain of a functio...
fnexALT 5921 If the domain of a functio...
funex 5922 If the domain of a functio...
opabex 5923 Existence of a function ex...
mptexg 5924 If the domain of a functio...
mptex 5925 If the domain of a functio...
funrnex 5926 If the domain of a functio...
zfrep6 5927 A version of the Axiom of ...
fex 5928 If the domain of a mapping...
fornex 5929 If the domain of an onto f...
f1dmex 5930 If the codomain of a one-t...
eufnfv 5931 A function is uniquely det...
funfvima 5932 A function's value in a pr...
funfvima2 5933 A function's value in an i...
funfvima3 5934 A class including a functi...
fnfvima 5935 The function value of an o...
rexima 5936 Existential quantification...
ralima 5937 Universal quantification u...
idref 5938 TODO: This is the same as...
fvclss 5939 Upper bound for the class ...
fvclex 5940 Existence of the class of ...
fvresex 5941 Existence of the class of ...
abrexex 5942 Existence of a class abstr...
abrexexg 5943 Existence of a class abstr...
elabrex 5944 Elementhood in an image se...
abrexco 5945 Composition of two image m...
iunexg 5946 The existence of an indexe...
abrexex2g 5947 Existence of an existentia...
opabex3d 5948 Existence of an ordered pa...
opabex3 5949 Existence of an ordered pa...
iunex 5950 The existence of an indexe...
imaiun 5951 The image of an indexed un...
imauni 5952 The image of a union is th...
fniunfv 5953 The indexed union of a fun...
funiunfv 5954 The indexed union of a fun...
funiunfvf 5955 The indexed union of a fun...
eluniima 5956 Membership in the union of...
elunirn 5957 Membership in the union of...
fnunirn 5958 Membership in a union of s...
elunirnALT 5959 Membership in the union of...
abrexex2 5960 Existence of an existentia...
abexssex 5961 Existence of a class abstr...
abexex 5962 A condition where a class ...
dff13 5963 A one-to-one function in t...
f1veqaeq 5964 If the values of a one-to-...
dff13f 5965 A one-to-one function in t...
f1mpt 5966 Express injection for a ma...
f1fveq 5967 Equality of function value...
f1elima 5968 Membership in the image of...
f1imass 5969 Taking images under a one-...
f1imaeq 5970 Taking images under a one-...
f1imapss 5971 Taking images under a one-...
dff1o6 5972 A one-to-one onto function...
f1ocnvfv1 5973 The converse value of the ...
f1ocnvfv2 5974 The value of the converse ...
f1ocnvfv 5975 Relationship between the v...
f1ocnvfvb 5976 Relationship between the v...
f1ocnvdm 5977 The value of the converse ...
f1ocnvfvrneq 5978 If the values of a one-to-...
fcof1 5979 An application is injectiv...
fcofo 5980 An application is surjecti...
cbvfo 5981 Change bound variable betw...
cbvexfo 5982 Change bound variable betw...
cocan1 5983 An injection is left-cance...
cocan2 5984 A surjection is right-canc...
fcof1o 5985 Show that two functions ar...
foeqcnvco 5986 Condition for function equ...
f1eqcocnv 5987 Condition for function equ...
fveqf1o 5988 Given a bijection ` F ` , ...
fliftrel 5989 ` F ` , a function lift, i...
fliftel 5990 Elementhood in the relatio...
fliftel1 5991 Elementhood in the relatio...
fliftcnv 5992 Converse of the relation `...
fliftfun 5993 The function ` F ` is the ...
fliftfund 5994 The function ` F ` is the ...
fliftfuns 5995 The function ` F ` is the ...
fliftf 5996 The domain and range of th...
fliftval 5997 The value of the function ...
isoeq1 5998 Equality theorem for isomo...
isoeq2 5999 Equality theorem for isomo...
isoeq3 6000 Equality theorem for isomo...
isoeq4 6001 Equality theorem for isomo...
isoeq5 6002 Equality theorem for isomo...
nfiso 6003 Bound-variable hypothesis ...
isof1o 6004 An isomorphism is a one-to...
isorel 6005 An isomorphism connects bi...
soisores 6006 Express the condition of i...
soisoi 6007 Infer isomorphism from one...
isoid 6008 Identity law for isomorphi...
isocnv 6009 Converse law for isomorphi...
isocnv2 6010 Converse law for isomorphi...
isocnv3 6011 Complementation law for is...
isores2 6012 An isomorphism from one we...
isores1 6013 An isomorphism from one we...
isores3 6014 Induced isomorphism on a s...
isotr 6015 Composition (transitive) l...
isomin 6016 Isomorphisms preserve mini...
isoini 6017 Isomorphisms preserve init...
isoini2 6018 Isomorphisms are isomorphi...
isofrlem 6019 Lemma for ~ isofr . (Cont...
isoselem 6020 Lemma for ~ isose . (Cont...
isofr 6021 An isomorphism preserves w...
isose 6022 An isomorphism preserves s...
isofr2 6023 A weak form of ~ isofr tha...
isopolem 6024 Lemma for ~ isopo . (Cont...
isopo 6025 An isomorphism preserves p...
isosolem 6026 Lemma for ~ isoso . (Cont...
isoso 6027 An isomorphism preserves s...
isowe 6028 An isomorphism preserves w...
isowe2 6029 A weak form of ~ isowe tha...
f1oiso 6030 Any one-to-one onto functi...
f1oiso2 6031 Any one-to-one onto functi...
f1owe 6032 Well-ordering of isomorphi...
f1oweALT 6033 Well-ordering of isomorphi...
weniso 6034 A set-like well-ordering h...
weisoeq 6035 Thus, there is at most one...
weisoeq2 6036 Thus, there is at most one...
wemoiso 6037 Thus, there is at most one...
wemoiso2 6038 Thus, there is at most one...
knatar 6039 The Knaster-Tarski theorem...
oveq 6046 Equality theorem for opera...
oveq1 6047 Equality theorem for opera...
oveq2 6048 Equality theorem for opera...
oveq12 6049 Equality theorem for opera...
oveq1i 6050 Equality inference for ope...
oveq2i 6051 Equality inference for ope...
oveq12i 6052 Equality inference for ope...
oveqi 6053 Equality inference for ope...
oveq123i 6054 Equality inference for ope...
oveq1d 6055 Equality deduction for ope...
oveq2d 6056 Equality deduction for ope...
oveqd 6057 Equality deduction for ope...
oveq12d 6058 Equality deduction for ope...
oveqan12d 6059 Equality deduction for ope...
oveqan12rd 6060 Equality deduction for ope...
oveq123d 6061 Equality deduction for ope...
nfovd 6062 Deduction version of bound...
nfov 6063 Bound-variable hypothesis ...
oprabid 6064 The law of concretion. Sp...
ovex 6065 The result of an operation...
ovssunirn 6066 The result of an operation...
ovprc 6067 The value of an operation ...
ovprc1 6068 The value of an operation ...
ovprc2 6069 The value of an operation ...
ovrcl 6070 Reverse closure for an ope...
csbovg 6071 Move class substitution in...
csbov12g 6072 Move class substitution in...
csbov1g 6073 Move class substitution in...
csbov2g 6074 Move class substitution in...
rspceov 6075 A frequently used special ...
fnotovb 6076 Equivalence of operation v...
opabbrex 6077 A collection of ordered pa...
0neqopab 6078 The empty set is never an ...
brabv 6079 If two classes are in a re...
dfoprab2 6080 Class abstraction for oper...
reloprab 6081 An operation class abstrac...
nfoprab1 6082 The abstraction variables ...
nfoprab2 6083 The abstraction variables ...
nfoprab3 6084 The abstraction variables ...
nfoprab 6085 Bound-variable hypothesis ...
oprabbid 6086 Equivalent wff's yield equ...
oprabbidv 6087 Equivalent wff's yield equ...
oprabbii 6088 Equivalent wff's yield equ...
ssoprab2 6089 Equivalence of ordered pai...
ssoprab2b 6090 Equivalence of ordered pai...
eqoprab2b 6091 Equivalence of ordered pai...
mpt2eq123 6092 An equality theorem for th...
mpt2eq12 6093 An equality theorem for th...
mpt2eq123dva 6094 An equality deduction for ...
mpt2eq123dv 6095 An equality deduction for ...
mpt2eq123i 6096 An equality inference for ...
mpt2eq3dva 6097 Slightly more general equa...
mpt2eq3ia 6098 An equality inference for ...
nfmpt21 6099 Bound-variable hypothesis ...
nfmpt22 6100 Bound-variable hypothesis ...
nfmpt2 6101 Bound-variable hypothesis ...
oprab4 6102 Two ways to state the doma...
cbvoprab1 6103 Rule used to change first ...
cbvoprab2 6104 Change the second bound va...
cbvoprab12 6105 Rule used to change first ...
cbvoprab12v 6106 Rule used to change first ...
cbvoprab3 6107 Rule used to change the th...
cbvoprab3v 6108 Rule used to change the th...
cbvmpt2x 6109 Rule to change the bound v...
cbvmpt2 6110 Rule to change the bound v...
cbvmpt2v 6111 Rule to change the bound v...
elimdelov 6112 Eliminate a hypothesis whi...
dmoprab 6113 The domain of an operation...
dmoprabss 6114 The domain of an operation...
rnoprab 6115 The range of an operation ...
rnoprab2 6116 The range of a restricted ...
reldmoprab 6117 The domain of an operation...
oprabss 6118 Structure of an operation ...
eloprabga 6119 The law of concretion for ...
eloprabg 6120 The law of concretion for ...
ssoprab2i 6121 Inference of operation cla...
mpt2v 6122 Operation with universal d...
mpt2mptx 6123 Express a two-argument fun...
mpt2mpt 6124 Express a two-argument fun...
resoprab 6125 Restriction of an operatio...
resoprab2 6126 Restriction of an operator...
resmpt2 6127 Restriction of the mapping...
funoprabg 6128 "At most one" is a suffici...
funoprab 6129 "At most one" is a suffici...
fnoprabg 6130 Functionality and domain o...
mpt2fun 6131 The maps-to notation for a...
fnoprab 6132 Functionality and domain o...
ffnov 6133 An operation maps to a cla...
fovcl 6134 Closure law for an operati...
eqfnov 6135 Equality of two operations...
eqfnov2 6136 Two operators with the sam...
fnov 6137 Representation of a functi...
mpt22eqb 6138 Bidirectional equality the...
rnmpt2 6139 The range of an operation ...
reldmmpt2 6140 The domain of an operation...
elrnmpt2g 6141 Membership in the range of...
elrnmpt2 6142 Membership in the range of...
ralrnmpt2 6143 A restricted quantifier ov...
rexrnmpt2 6144 A restricted quantifier ov...
oprabexd 6145 Existence of an operator a...
oprabex 6146 Existence of an operation ...
oprabex3 6147 Existence of an operation ...
oprabrexex2 6148 Existence of an existentia...
ovid 6149 The value of an operation ...
ovidig 6150 The value of an operation ...
ovidi 6151 The value of an operation ...
ov 6152 The value of an operation ...
ovigg 6153 The value of an operation ...
ovig 6154 The value of an operation ...
ovmpt4g 6155 Value of a function given ...
ovmpt2s 6156 Value of a function given ...
ov2gf 6157 The value of an operation ...
ovmpt2dxf 6158 Value of an operation give...
ovmpt2dx 6159 Value of an operation give...
ovmpt2d 6160 Value of an operation give...
ovmpt2x 6161 The value of an operation ...
ovmpt2ga 6162 Value of an operation give...
ovmpt2a 6163 Value of an operation give...
ovmpt2df 6164 Alternate deduction versio...
ovmpt2dv 6165 Alternate deduction versio...
ovmpt2dv2 6166 Alternate deduction versio...
ovmpt2g 6167 Value of an operation give...
ovmpt2 6168 Value of an operation give...
ov3 6169 The value of an operation ...
ov6g 6170 The value of an operation ...
ovg 6171 The value of an operation ...
ovres 6172 The value of a restricted ...
ovresd 6173 Lemma for converting metri...
oprssov 6174 The value of a member of t...
fovrn 6175 An operation's value belon...
fovrnda 6176 An operation's value belon...
fovrnd 6177 An operation's value belon...
fnrnov 6178 The range of an operation ...
foov 6179 An onto mapping of an oper...
fnovrn 6180 An operation's value belon...
ovelrn 6181 A member of an operation's...
funimassov 6182 Membership relation for th...
ovelimab 6183 Operation value in an imag...
ovconst2 6184 The value of a constant op...
ab2rexex 6185 Existence of a class abstr...
ab2rexex2 6186 Existence of an existentia...
oprssdm 6187 Domain of closure of an op...
nssdmovg 6188 The value of an operation ...
ndmovg 6189 The value of an operation ...
ndmov 6190 The value of an operation ...
ndmovcl 6191 The closure of an operatio...
ndmovrcl 6192 Reverse closure law, when ...
ndmovcom 6193 Any operation is commutati...
ndmovass 6194 Any operation is associati...
ndmovdistr 6195 Any operation is distribut...
ndmovord 6196 Elimination of redundant a...
ndmovordi 6197 Elimination of redundant a...
caovclg 6198 Convert an operation closu...
caovcld 6199 Convert an operation closu...
caovcl 6200 Convert an operation closu...
caovcomg 6201 Convert an operation commu...
caovcomd 6202 Convert an operation commu...
caovcom 6203 Convert an operation commu...
caovassg 6204 Convert an operation assoc...
caovassd 6205 Convert an operation assoc...
caovass 6206 Convert an operation assoc...
caovcang 6207 Convert an operation cance...
caovcand 6208 Convert an operation cance...
caovcanrd 6209 Commute the arguments of a...
caovcan 6210 Convert an operation cance...
caovordig 6211 Convert an operation order...
caovordid 6212 Convert an operation order...
caovordg 6213 Convert an operation order...
caovordd 6214 Convert an operation order...
caovord2d 6215 Operation ordering law wit...
caovord3d 6216 Ordering law. (Contribute...
caovord 6217 Convert an operation order...
caovord2 6218 Operation ordering law wit...
caovord3 6219 Ordering law. (Contribute...
caovdig 6220 Convert an operation distr...
caovdid 6221 Convert an operation distr...
caovdir2d 6222 Convert an operation distr...
caovdirg 6223 Convert an operation rever...
caovdird 6224 Convert an operation distr...
caovdi 6225 Convert an operation distr...
caov32d 6226 Rearrange arguments in a c...
caov12d 6227 Rearrange arguments in a c...
caov31d 6228 Rearrange arguments in a c...
caov13d 6229 Rearrange arguments in a c...
caov4d 6230 Rearrange arguments in a c...
caov411d 6231 Rearrange arguments in a c...
caov42d 6232 Rearrange arguments in a c...
caov32 6233 Rearrange arguments in a c...
caov12 6234 Rearrange arguments in a c...
caov31 6235 Rearrange arguments in a c...
caov13 6236 Rearrange arguments in a c...
caov4 6237 Rearrange arguments in a c...
caov411 6238 Rearrange arguments in a c...
caov42 6239 Rearrange arguments in a c...
caovdir 6240 Reverse distributive law. ...
caovdilem 6241 Lemma used by real number ...
caovlem2 6242 Lemma used in real number ...
caovmo 6243 Uniqueness of inverse elem...
grprinvlem 6244 Lemma for ~ grprinvd . (C...
grprinvd 6245 Deduce right inverse from ...
grpridd 6246 Deduce right identity from...
elmpt2cl 6247 If a two-parameter class i...
elmpt2cl1 6248