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