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

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