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