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