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

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