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

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