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...
ax12b 1834 Two equivalent ways of exp...
ax10o 1835 Show that ~ ax-10o can be ...
ax10from10o 1837 Rederivation of ~ ax-10 fr...
alequcom-o 1838 Commutation law for identi...
alequcoms-o 1839 A commutation rule for ide...
nalequcoms-o 1840 A commutation rule for dis...
hbae 1841 All variables are effectiv...
hbae-o 1842 All variables are effectiv...
nfae 1843 All variables are effectiv...
hbaes 1844 Rule that applies ~ hbae t...
hbnae 1845 All variables are effectiv...
hbnae-o 1846 All variables are effectiv...
nfnae 1847 All variables are effectiv...
hbnaes 1848 Rule that applies ~ hbnae ...
nfeqf 1849 A variable is effectively ...
equs4 1850 Lemma used in proofs of su...
equsal 1851 A useful equivalence relat...
equsalh 1852 A useful equivalence relat...
equsex 1853 A useful equivalence relat...
dvelimfALT 1854 Proof of ~ dvelimh that us...
dvelimf-o 1855 Proof of ~ dvelimh that us...
dral1 1856 Formula-building lemma for...
dral1-o 1857 Formula-building lemma for...
dral2 1858 Formula-building lemma for...
dral2-o 1859 Formula-building lemma for...
drex1 1860 Formula-building lemma for...
drex2 1861 Formula-building lemma for...
drnf1 1862 Formula-building lemma for...
drnf2 1863 Formula-building lemma for...
exdistrf 1864 Distribution of existentia...
nfald2 1865 Variation on ~ nfald which...
nfexd2 1866 Variation on ~ nfexd which...
a4imt 1867 Closed theorem form of ~ a...
a4im 1868 Specialization, using impl...
a4ime 1869 Existential introduction, ...
a4imed 1870 Deduction version of ~ a4i...
cbv1h 1871 Rule used to change bound ...
cbv1 1872 Rule used to change bound ...
cbv2h 1873 Rule used to change bound ...
cbv2 1874 Rule used to change bound ...
cbv3 1875 Rule used to change bound ...
cbv3ALT 1876 Rule used to change bound ...
cbval 1877 Rule used to change bound ...
cbvex 1878 Rule used to change bound ...
chvar 1879 Implicit substitution of `...
equvini 1880 A variable introduction la...
equveli 1881 A variable elimination law...
ax12 1882 Derive ~ ax-12 from ~ ax-1...
sbimi 1885 Infer substitution into an...
sbbii 1886 Infer substitution into bo...
drsb1 1887 Formula-building lemma for...
sb1 1888 One direction of a simplif...
sb2 1889 One direction of a simplif...
sbequ1 1890 An equality theorem for su...
sbequ2 1891 An equality theorem for su...
stdpc7 1892 One of the two equality ax...
sbequ12 1893 An equality theorem for su...
sbequ12r 1894 An equality theorem for su...
sbequ12a 1895 An equality theorem for su...
sbid 1896 An identity theorem for su...
stdpc4 1897 The specialization axiom o...
sbft 1898 Substitution has no effect...
sbf 1899 Substitution for a variabl...
sbh 1900 Substitution for a variabl...
sbf2 1901 Substitution has no effect...
sb6x 1902 Equivalence involving subs...
nfs1f 1903 If ` x ` is not free in ` ...
sbequ5 1904 Substitution does not chan...
sbequ6 1905 Substitution does not chan...
sbt 1906 A substitution into a theo...
equsb1 1907 Substitution applied to an...
equsb2 1908 Substitution applied to an...
sbied 1909 Conversion of implicit sub...
sbiedv 1910 Conversion of implicit sub...
sbie 1911 Conversion of implicit sub...
equs5a 1912 A property related to subs...
equs5e 1913 A property related to subs...
sb4a 1914 A version of ~ sb4 that do...
equs45f 1915 Two ways of expressing sub...
sb6f 1916 Equivalence for substituti...
sb5f 1917 Equivalence for substituti...
sb4e 1918 One direction of a simplif...
hbsb2a 1919 Special case of a bound-va...
hbsb2e 1920 Special case of a bound-va...
hbsb3 1921 If ` y ` is not free in ` ...
nfs1 1922 If ` y ` is not free in ` ...
a4imv 1923 A version of ~ a4im with a...
aev 1924 A "distinctor elimination"...
aev-o 1925 A "distinctor elimination"...
ax16 1926 Theorem showing that ~ ax-...
ax17eq 1928 Theorem to add distinct qu...
dveeq2 1929 Quantifier introduction wh...
dveeq2-o 1930 Quantifier introduction wh...
dveeq2ALT 1931 Version of ~ dveeq2 using ...
nd5 1932 A lemma for proving condit...
exlimdv 1933 Deduction from Theorem 19....
exlimdd 1934 Existential elimination ru...
exlimddv 1935 Existential elimination ru...
ax11v2 1936 Recovery of ~ ax-11o from ...
ax11v2-o 1937 Recovery of ~ ax-11o from ...
ax11a2 1938 Derive ~ ax-11o from a hyp...
ax11a2-o 1939 Derive ~ ax-11o from a hyp...
ax11o 1940 Derivation of set.mm's ori...
ax11 1942 Rederivation of axiom ~ ax...
ax11b 1943 A bidirectional version of...
equs5 1944 Lemma used in proofs of su...
sb3 1945 One direction of a simplif...
sb4 1946 One direction of a simplif...
sb4b 1947 Simplified definition of s...
dfsb2 1948 An alternate definition of...
dfsb3 1949 An alternate definition of...
hbsb2 1950 Bound-variable hypothesis ...
nfsb2 1951 Bound-variable hypothesis ...
sbequi 1952 An equality theorem for su...
sbequ 1953 An equality theorem for su...
drsb2 1954 Formula-building lemma for...
sbn 1955 Negation inside and outsid...
sbi1 1956 Removal of implication fro...
sbi2 1957 Introduction of implicatio...
sbim 1958 Implication inside and out...
sbor 1959 Logical OR inside and outs...
sbrim 1960 Substitution with a variab...
sblim 1961 Substitution with a variab...
sban 1962 Conjunction inside and out...
sb3an 1963 Conjunction inside and out...
sbbi 1964 Equivalence inside and out...
sblbis 1965 Introduce left bicondition...
sbrbis 1966 Introduce right biconditio...
sbrbif 1967 Introduce right biconditio...
a4sbe 1968 A specialization theorem. ...
a4sbim 1969 Specialization of implicat...
a4sbbi 1970 Specialization of bicondit...
sbbid 1971 Deduction substituting bot...
sbequ8 1972 Elimination of equality fr...
nfsb4t 1973 A variable not free remain...
nfsb4 1974 A variable not free remain...
dvelimh 1975 Version of ~ dvelim withou...
dvelimf 1976 Version of ~ dvelimv witho...
dvelimdf 1977 Deduction form of ~ dvelim...
sbco 1978 A composition law for subs...
sbid2 1979 An identity law for substi...
sbidm 1980 An idempotent law for subs...
sbco2 1981 A composition law for subs...
sbco2d 1982 A composition law for subs...
sbco3 1983 A composition law for subs...
sbcom 1984 A commutativity law for su...
sb5rf 1985 Reversed substitution. (C...
sb6rf 1986 Reversed substitution. (C...
sb8 1987 Substitution of variable i...
sb8e 1988 Substitution of variable i...
sb9i 1989 Commutation of quantificat...
sb9 1990 Commutation of quantificat...
ax11v 1991 This is a version of ~ ax-...
sb56 1992 Two equivalent ways of exp...
sb6 1993 Equivalence for substituti...
sb5 1994 Equivalence for substituti...
ax16i 1995 Inference with ~ ax-16 as ...
ax16ALT 1996 Version of ~ ax16 that doe...
a4v 1997 Specialization, using impl...
a4imev 1998 Distinct-variable version ...
a4eiv 1999 Inference from existential...
equvin 2000 A variable introduction la...
a16g 2001 A generalization of axiom ...
a16g-o 2002 A generalization of axiom ...
a16gb 2003 A generalization of axiom ...
a16nf 2004 If ~ dtru is false, then t...
albidv 2005 Formula-building rule for ...
exbidv 2006 Formula-building rule for ...
2albidv 2007 Formula-building rule for ...
2exbidv 2008 Formula-building rule for ...
3exbidv 2009 Formula-building rule for ...
4exbidv 2010 Formula-building rule for ...
19.9v 2011 Special case of Theorem 19...
19.21v 2012 Special case of Theorem 19...
alrimiv 2013 Inference from Theorem 19....
alrimivv 2014 Inference from Theorem 19....
alrimdv 2015 Deduction from Theorem 19....
nfdv 2016 Apply the definition of no...
2ax17 2017 Quantification of two vari...
alimdv 2018 Deduction from Theorem 19....
eximdv 2019 Deduction from Theorem 19....
2alimdv 2020 Deduction from Theorem 19....
2eximdv 2021 Deduction from Theorem 19....
19.23v 2022 Special case of Theorem 19...
19.23vv 2023 Theorem 19.23 of [Margaris...
exlimiv 2024 Inference from Theorem 19....
pm11.53 2025 Theorem *11.53 in [Whitehe...
exlimivv 2026 Inference from Theorem 19....
exlimdvv 2027 Deduction from Theorem 19....
19.27v 2028 Theorem 19.27 of [Margaris...
19.28v 2029 Theorem 19.28 of [Margaris...
19.36v 2030 Special case of Theorem 19...
19.36aiv 2031 Inference from Theorem 19....
19.12vv 2032 Special case of ~ 19.12 wh...
19.37v 2033 Special case of Theorem 19...
19.37aiv 2034 Inference from Theorem 19....
19.41v 2035 Special case of Theorem 19...
19.41vv 2036 Theorem 19.41 of [Margaris...
19.41vvv 2037 Theorem 19.41 of [Margaris...
19.41vvvv 2038 Theorem 19.41 of [Margaris...
19.42v 2039 Special case of Theorem 19...
exdistr 2040 Distribution of existentia...
19.42vv 2041 Theorem 19.42 of [Margaris...
19.42vvv 2042 Theorem 19.42 of [Margaris...
exdistr2 2043 Distribution of existentia...
3exdistr 2044 Distribution of existentia...
4exdistr 2045 Distribution of existentia...
cbvalv 2046 Rule used to change bound ...
cbvexv 2047 Rule used to change bound ...
cbval2 2048 Rule used to change bound ...
cbvex2 2049 Rule used to change bound ...
cbval2v 2050 Rule used to change bound ...
cbvex2v 2051 Rule used to change bound ...
cbvald 2052 Deduction used to change b...
cbvexd 2053 Deduction used to change b...
cbvaldva 2054 Rule used to change the bo...
cbvexdva 2055 Rule used to change the bo...
cbvex4v 2056 Rule used to change bound ...
eean 2057 Rearrange existential quan...
eeanv 2058 Rearrange existential quan...
eeeanv 2059 Rearrange existential quan...
ee4anv 2060 Rearrange existential quan...
nexdv 2061 Deduction for generalizati...
chvarv 2062 Implicit substitution of `...
cleljust 2063 When the class variables i...
equsb3lem 2064 Lemma for ~ equsb3 . (Con...
equsb3 2065 Substitution applied to an...
elsb3 2066 Substitution applied to an...
elsb4 2067 Substitution applied to an...
hbs1 2068 ` x ` is not free in ` [ y...
nfs1v 2069 ` x ` is not free in ` [ y...
sbhb 2070 Two ways of expressing " `...
sbnf2 2071 Two ways of expressing " `...
nfsb 2072 If ` z ` is not free in ` ...
hbsb 2073 If ` z ` is not free in ` ...
nfsbd 2074 Deduction version of ~ nfs...
2sb5 2075 Equivalence for double sub...
2sb6 2076 Equivalence for double sub...
sbcom2 2077 Commutativity law for subs...
pm11.07 2078 Theorem *11.07 in [Whitehe...
sb6a 2079 Equivalence for substituti...
2sb5rf 2080 Reversed double substituti...
2sb6rf 2081 Reversed double substituti...
dfsb7 2082 An alternate definition of...
sb7f 2083 This version of ~ dfsb7 do...
sb7h 2084 This version of ~ dfsb7 do...
sb10f 2085 Hao Wang's identity axiom ...
sbid2v 2086 An identity law for substi...
sbelx 2087 Elimination of substitutio...
sbel2x 2088 Elimination of double subs...
sbal1 2089 A theorem used in eliminat...
sbal 2090 Move universal quantifier ...
sbex 2091 Move existential quantifie...
sbalv 2092 Quantify with new variable...
exsb 2093 An equivalent expression f...
exsbOLD 2094 An equivalent expression f...
2exsb 2095 An equivalent expression f...
dvelim 2096 This theorem can be used t...
dvelimv 2097 This theorem can be used t...
dvelimALT 2098 Version of ~ dvelim that d...
dveeq1 2099 Quantifier introduction wh...
dveeq1-o 2100 Quantifier introduction wh...
dveeq1ALT 2101 Version of ~ dveeq1 using ...
dveel1 2102 Quantifier introduction wh...
dveel2 2103 Quantifier introduction wh...
sbal2 2104 Move quantifier in and out...
ax15 2105 Axiom ~ ax-15 is redundant...
ax17el 2107 Theorem to add distinct qu...
dveel2ALT 2108 Version of ~ dveel2 using ...
ax11eq 2109 Basis step for constructin...
ax11el 2110 Basis step for constructin...
ax11f 2111 Basis step for constructin...
ax11indn 2112 Induction step for constru...
ax11indi 2113 Induction step for constru...
ax11indalem 2114 Lemma for ~ ax11inda2 and ...
ax11inda2ALT 2115 A proof of ~ ax11inda2 tha...
ax11inda2 2116 Induction step for constru...
ax11inda 2117 Induction step for constru...
eujust 2120 A soundness justification ...
eujustALT 2121 A soundness justification ...
euf 2124 A version of the existenti...
eubid 2125 Formula-building rule for ...
eubidv 2126 Formula-building rule for ...
eubii 2127 Introduce uniqueness quant...
nfeu1 2128 Bound-variable hypothesis ...
nfmo1 2129 Bound-variable hypothesis ...
nfeud2 2130 Bound-variable hypothesis ...
nfmod2 2131 Bound-variable hypothesis ...
nfeud 2132 Deduction version of ~ nfe...
nfmod 2133 Bound-variable hypothesis ...
nfeu 2134 Bound-variable hypothesis ...
nfmo 2135 Bound-variable hypothesis ...
sb8eu 2136 Variable substitution in u...
sb8mo 2137 Variable substitution in u...
cbveu 2138 Rule used to change bound ...
eu1 2139 An alternate way to expres...
mo 2140 Equivalent definitions of ...
euex 2141 Existential uniqueness imp...
eumo0 2142 Existential uniqueness imp...
eu2 2143 An alternate way of defini...
eu3 2144 An alternate way to expres...
euor 2145 Introduce a disjunct into ...
euorv 2146 Introduce a disjunct into ...
mo2 2147 Alternate definition of "a...
sbmo 2148 Substitution into "at most...
mo3 2149 Alternate definition of "a...
mo4f 2150 "At most one" expressed us...
mo4 2151 "At most one" expressed us...
mobid 2152 Formula-building rule for ...
mobidv 2153 Formula-building rule for ...
mobii 2154 Formula-building rule for ...
cbvmo 2155 Rule used to change bound ...
eu5 2156 Uniqueness in terms of "at...
eu4 2157 Uniqueness using implicit ...
eumo 2158 Existential uniqueness imp...
eumoi 2159 "At most one" inferred fro...
exmoeu 2160 Existence in terms of "at ...
exmoeu2 2161 Existence implies "at most...
moabs 2162 Absorption of existence co...
exmo 2163 Something exists or at mos...
moim 2164 "At most one" is preserved...
moimi 2165 "At most one" is preserved...
morimv 2166 Move antecedent outside of...
euimmo 2167 Uniqueness implies "at mos...
euim 2168 Add existential uniqueness...
moan 2169 "At most one" is still the...
moani 2170 "At most one" is still tru...
moor 2171 "At most one" is still the...
mooran1 2172 "At most one" imports disj...
mooran2 2173 "At most one" exports disj...
moanim 2174 Introduction of a conjunct...
euan 2175 Introduction of a conjunct...
moanimv 2176 Introduction of a conjunct...
moaneu 2177 Nested "at most one" and u...
moanmo 2178 Nested "at most one" quant...
euanv 2179 Introduction of a conjunct...
mopick 2180 "At most one" picks a vari...
eupick 2181 Existential uniqueness "pi...
eupicka 2182 Version of ~ eupick with c...
eupickb 2183 Existential uniqueness "pi...
eupickbi 2184 Theorem *14.26 in [Whitehe...
mopick2 2185 "At most one" can show the...
euor2 2186 Introduce or eliminate a d...
moexex 2187 "At most one" double quant...
moexexv 2188 "At most one" double quant...
2moex 2189 Double quantification with...
2euex 2190 Double quantification with...
2eumo 2191 Double quantification with...
2eu2ex 2192 Double existential uniquen...
2moswap 2193 A condition allowing swap ...
2euswap 2194 A condition allowing swap ...
2exeu 2195 Double existential uniquen...
2mo 2196 Two equivalent expressions...
2mos 2197 Double "exists at most one...
2eu1 2198 Double existential uniquen...
2eu2 2199 Double existential uniquen...
2eu3 2200 Double existential uniquen...
2eu4 2201 This theorem provides us w...
2eu5 2202 An alternate definition of...
2eu6 2203 Two equivalent expressions...
2eu7 2204 Two equivalent expressions...
2eu8 2205 Two equivalent expressions...
euequ1 2206 Equality has existential u...
exists1 2207 Two ways to express "only ...
exists2 2208 A condition implying that ...
barbara 2215 "Barbara", one of the fund...
celarent 2216 "Celarent", one of the syl...
darii 2217 "Darii", one of the syllog...
ferio 2218 "Ferio" ("Ferioque"), one ...
barbari 2219 "Barbari", one of the syll...
celaront 2220 "Celaront", one of the syl...
cesare 2221 "Cesare", one of the syllo...
camestres 2222 "Camestres", one of the sy...
festino 2223 "Festino", one of the syll...
baroco 2224 "Baroco", one of the syllo...
cesaro 2225 "Cesaro", one of the syllo...
camestros 2226 "Camestros", one of the sy...
datisi 2227 "Datisi", one of the syllo...
disamis 2228 "Disamis", one of the syll...
ferison 2229 "Ferison", one of the syll...
bocardo 2230 "Bocardo", one of the syll...
felapton 2231 "Felapton", one of the syl...
darapti 2232 "Darapti", one of the syll...
calemes 2233 "Calemes", one of the syll...
dimatis 2234 "Dimatis", one of the syll...
fresison 2235 "Fresison", one of the syl...
calemos 2236 "Calemos", one of the syll...
fesapo 2237 "Fesapo", one of the syllo...
bamalip 2238 "Bamalip", one of the syll...
axext2 2240 The Axiom of Extensionalit...
axext3 2241 A generalization of the Ax...
axext4 2242 A bidirectional version of...
bm1.1 2243 Any set defined by a prope...
abid 2246 Simplification of class ab...
hbab1 2247 Bound-variable hypothesis ...
nfsab1 2248 Bound-variable hypothesis ...
hbab 2249 Bound-variable hypothesis ...
nfsab 2250 Bound-variable hypothesis ...
dfcleq 2252 The same as ~ df-cleq with...
cvjust 2253 Every set is a class. Pro...
eqriv 2255 Infer equality of classes ...
eqrdv 2256 Deduce equality of classes...
eqrdav 2257 Deduce equality of classes...
eqid 2258 Law of identity (reflexivi...
eqidd 2259 Class identity law with an...
eqcom 2260 Commutative law for class ...
eqcoms 2261 Inference applying commuta...
eqcomi 2262 Inference from commutative...
eqcomd 2263 Deduction from commutative...
eqeq1 2264 Equality implies equivalen...
eqeq1i 2265 Inference from equality to...
eqeq1d 2266 Deduction from equality to...
eqeq2 2267 Equality implies equivalen...
eqeq2i 2268 Inference from equality to...
eqeq2d 2269 Deduction from equality to...
eqeq12 2270 Equality relationship amon...
eqeq12i 2271 A useful inference for sub...
eqeq12d 2272 A useful inference for sub...
eqeqan12d 2273 A useful inference for sub...
eqeqan12rd 2274 A useful inference for sub...
eqtr 2275 Transitive law for class e...
eqtr2 2276 A transitive law for class...
eqtr3 2277 A transitive law for class...
eqtri 2278 An equality transitivity i...
eqtr2i 2279 An equality transitivity i...
eqtr3i 2280 An equality transitivity i...
eqtr4i 2281 An equality transitivity i...
3eqtri 2282 An inference from three ch...
3eqtrri 2283 An inference from three ch...
3eqtr2i 2284 An inference from three ch...
3eqtr2ri 2285 An inference from three ch...
3eqtr3i 2286 An inference from three ch...
3eqtr3ri 2287 An inference from three ch...
3eqtr4i 2288 An inference from three ch...
3eqtr4ri 2289 An inference from three ch...
eqtrd 2290 An equality transitivity d...
eqtr2d 2291 An equality transitivity d...
eqtr3d 2292 An equality transitivity e...
eqtr4d 2293 An equality transitivity e...
3eqtrd 2294 A deduction from three cha...
3eqtrrd 2295 A deduction from three cha...
3eqtr2d 2296 A deduction from three cha...
3eqtr2rd 2297 A deduction from three cha...
3eqtr3d 2298 A deduction from three cha...
3eqtr3rd 2299 A deduction from three cha...
3eqtr4d 2300 A deduction from three cha...
3eqtr4rd 2301 A deduction from three cha...
syl5eq 2302 An equality transitivity d...
syl5req 2303 An equality transitivity d...
syl5eqr 2304 An equality transitivity d...
syl5reqr 2305 An equality transitivity d...
syl6eq 2306 An equality transitivity d...
syl6req 2307 An equality transitivity d...
syl6eqr 2308 An equality transitivity d...
syl6reqr 2309 An equality transitivity d...
sylan9eq 2310 An equality transitivity d...
sylan9req 2311 An equality transitivity d...
sylan9eqr 2312 An equality transitivity d...
3eqtr3g 2313 A chained equality inferen...
3eqtr3a 2314 A chained equality inferen...
3eqtr4g 2315 A chained equality inferen...
3eqtr4a 2316 A chained equality inferen...
eq2tri 2317 A compound transitive infe...
eleq1 2318 Equality implies equivalen...
eleq2 2319 Equality implies equivalen...
eleq12 2320 Equality implies equivalen...
eleq1i 2321 Inference from equality to...
eleq2i 2322 Inference from equality to...
eleq12i 2323 Inference from equality to...
eleq1d 2324 Deduction from equality to...
eleq2d 2325 Deduction from equality to...
eleq12d 2326 Deduction from equality to...
eleq1a 2327 A transitive-type law rela...
eqeltri 2328 Substitution of equal clas...
eqeltrri 2329 Substitution of equal clas...
eleqtri 2330 Substitution of equal clas...
eleqtrri 2331 Substitution of equal clas...
eqeltrd 2332 Substitution of equal clas...
eqeltrrd 2333 Deduction that substitutes...
eleqtrd 2334 Deduction that substitutes...
eleqtrrd 2335 Deduction that substitutes...
3eltr3i 2336 Substitution of equal clas...
3eltr4i 2337 Substitution of equal clas...
3eltr3d 2338 Substitution of equal clas...
3eltr4d 2339 Substitution of equal clas...
3eltr3g 2340 Substitution of equal clas...
3eltr4g 2341 Substitution of equal clas...
syl5eqel 2342 B membership and equality ...
syl5eqelr 2343 B membership and equality ...
syl5eleq 2344 B membership and equality ...
syl5eleqr 2345 B membership and equality ...
syl6eqel 2346 A membership and equality ...
syl6eqelr 2347 A membership and equality ...
syl6eleq 2348 A membership and equality ...
syl6eleqr 2349 A membership and equality ...
eleq2s 2350 Substitution of equal clas...
eqneltrd 2351 If a class is not an eleme...
eqneltrrd 2352 If a class is not an eleme...
neleqtrd 2353 If a class is not an eleme...
neleqtrrd 2354 If a class is not an eleme...
cleqh 2355 Establish equality between...
nelneq 2356 A way of showing two class...
nelneq2 2357 A way of showing two class...
eqsb3lem 2358 Lemma for ~ eqsb3 . (Cont...
eqsb3 2359 Substitution applied to an...
clelsb3 2360 Substitution applied to an...
hbxfreq 2361 A utility lemma to transfe...
hblem 2362 Change the free variable o...
abeq2 2363 Equality of a class variab...
abeq1 2364 Equality of a class variab...
abeq2i 2365 Equality of a class variab...
abeq1i 2366 Equality of a class variab...
abeq2d 2367 Equality of a class variab...
abbi 2368 Equivalent wff's correspon...
abbi2i 2369 Equality of a class variab...
abbii 2370 Equivalent wff's yield equ...
abbid 2371 Equivalent wff's yield equ...
abbidv 2372 Equivalent wff's yield equ...
abbi2dv 2373 Deduction from a wff to a ...
abbi1dv 2374 Deduction from a wff to a ...
abid2 2375 A simplification of class ...
cbvab 2376 Rule used to change bound ...
cbvabv 2377 Rule used to change bound ...
clelab 2378 Membership of a class vari...
clabel 2379 Membership of a class abst...
sbab 2380 The right-hand side of the...
nfcjust 2382 Justification theorem for ...
nfci 2384 Deduce that a class ` A ` ...
nfcii 2385 Deduce that a class ` A ` ...
nfcr 2386 Consequence of the not-fre...
nfcrii 2387 Consequence of the not-fre...
nfcri 2388 Consequence of the not-fre...
nfcd 2389 Deduce that a class ` A ` ...
nfceqi 2390 Equality theorem for class...
nfcxfr 2391 A utility lemma to transfe...
nfcxfrd 2392 A utility lemma to transfe...
nfceqdf 2393 An equality theorem for ef...
nfcv 2394 If ` x ` is disjoint from ...
nfcvd 2395 If ` x ` is disjoint from ...
nfab1 2396 Bound-variable hypothesis ...
nfnfc1 2397 ` x ` is bound in ` F/_ x ...
nfab 2398 Bound-variable hypothesis ...
nfaba1 2399 Bound-variable hypothesis ...
nfnfc 2400 Hypothesis builder for ` F...
nfeq 2401 Hypothesis builder for equ...
nfel 2402 Hypothesis builder for ele...
nfeq1 2403 Hypothesis builder for equ...
nfel1 2404 Hypothesis builder for ele...
nfeq2 2405 Hypothesis builder for equ...
nfel2 2406 Hypothesis builder for ele...
nfcrd 2407 Consequence of the not-fre...
nfeqd 2408 Hypothesis builder for equ...
nfeld 2409 Hypothesis builder for ele...
drnfc1 2410 Formula-building lemma for...
drnfc2 2411 Formula-building lemma for...
nfabd2 2412 Bound-variable hypothesis ...
nfabd 2413 Bound-variable hypothesis ...
dvelimdc 2414 Deduction form of ~ dvelim...
dvelimc 2415 Version of ~ dvelim for cl...
nfcvf 2416 If ` x ` and ` y ` are dis...
nfcvf2 2417 If ` x ` and ` y ` are dis...
cleqf 2418 Establish equality between...
abid2f 2419 A simplification of class ...
sbabel 2420 Theorem to move a substitu...
nne 2425 Negation of inequality. (...
neirr 2426 No class is unequal to its...
exmidne 2427 Excluded middle with equal...
nonconne 2428 Law of noncontradiction wi...
neeq1 2429 Equality theorem for inequ...
neeq2 2430 Equality theorem for inequ...
neeq1i 2431 Inference for inequality. ...
neeq2i 2432 Inference for inequality. ...
neeq12i 2433 Inference for inequality. ...
neeq1d 2434 Deduction for inequality. ...
neeq2d 2435 Deduction for inequality. ...
neeq12d 2436 Deduction for inequality. ...
neneqd 2437 Deduction eliminating ineq...
eqnetri 2438 Substitution of equal clas...
eqnetrd 2439 Substitution of equal clas...
eqnetrri 2440 Substitution of equal clas...
eqnetrrd 2441 Substitution of equal clas...
neeqtri 2442 Substitution of equal clas...
neeqtrd 2443 Substitution of equal clas...
neeqtrri 2444 Substitution of equal clas...
neeqtrrd 2445 Substitution of equal clas...
syl5eqner 2446 B chained equality inferen...
3netr3d 2447 Substitution of equality i...
3netr4d 2448 Substitution of equality i...
3netr3g 2449 Substitution of equality i...
3netr4g 2450 Substitution of equality i...
necon3abii 2451 Deduction from equality to...
necon3bbii 2452 Deduction from equality to...
necon3bii 2453 Inference from equality to...
necon3abid 2454 Deduction from equality to...
necon3bbid 2455 Deduction from equality to...
necon3bid 2456 Deduction from equality to...
necon3ad 2457 Contrapositive law deducti...
necon3bd 2458 Contrapositive law deducti...
necon3d 2459 Contrapositive law deducti...
necon3i 2460 Contrapositive inference f...
necon3ai 2461 Contrapositive inference f...
necon3bi 2462 Contrapositive inference f...
necon1ai 2463 Contrapositive inference f...
necon1bi 2464 Contrapositive inference f...
necon1i 2465 Contrapositive inference f...
necon2ai 2466 Contrapositive inference f...
necon2bi 2467 Contrapositive inference f...
necon2i 2468 Contrapositive inference f...
necon2ad 2469 Contrapositive inference f...
necon2bd 2470 Contrapositive inference f...
necon2d 2471 Contrapositive inference f...
necon1abii 2472 Contrapositive inference f...
necon1bbii 2473 Contrapositive inference f...
necon1abid 2474 Contrapositive deduction f...
necon1bbid 2475 Contrapositive inference f...
necon2abii 2476 Contrapositive inference f...
necon2bbii 2477 Contrapositive inference f...
necon2abid 2478 Contrapositive deduction f...
necon2bbid 2479 Contrapositive deduction f...
necon4ai 2480 Contrapositive inference f...
necon4i 2481 Contrapositive inference f...
necon4ad 2482 Contrapositive inference f...
necon4bd 2483 Contrapositive inference f...
necon4d 2484 Contrapositive inference f...
necon4abid 2485 Contrapositive law deducti...
necon4bbid 2486 Contrapositive law deducti...
necon4bid 2487 Contrapositive law deducti...
necon1ad 2488 Contrapositive deduction f...
necon1bd 2489 Contrapositive deduction f...
necon1d 2490 Contrapositive law deducti...
neneqad 2491 If it is not the case that...
nebi 2492 Contraposition law for ine...
pm13.18 2493 Theorem *13.18 in [Whitehe...
pm13.181 2494 Theorem *13.181 in [Whiteh...
pm2.21ddne 2495 A contradiction implies an...
pm2.61ne 2496 Deduction eliminating an i...
pm2.61ine 2497 Inference eliminating an i...
pm2.61dne 2498 Deduction eliminating an i...
pm2.61dane 2499 Deduction eliminating an i...
pm2.61da2ne 2500 Deduction eliminating two ...
pm2.61da3ne 2501 Deduction eliminating thre...
necom 2502 Commutation of inequality....
necomi 2503 Inference from commutative...
necomd 2504 Deduction from commutative...
neor 2505 Logical OR with an equalit...
neanior 2506 A DeMorgan's law for inequ...
ne3anior 2507 A DeMorgan's law for inequ...
neorian 2508 A DeMorgan's law for inequ...
nemtbir 2509 An inference from an inequ...
nelne1 2510 Two classes are different ...
nelne2 2511 Two classes are different ...
neleq1 2512 Equality theorem for negat...
neleq2 2513 Equality theorem for negat...
nfne 2514 Bound-variable hypothesis ...
nfnel 2515 Bound-variable hypothesis ...
nfned 2516 Bound-variable hypothesis ...
nfneld 2517 Bound-variable hypothesis ...
ralnex 2528 Relationship between restr...
rexnal 2529 Relationship between restr...
dfral2 2530 Relationship between restr...
dfrex2 2531 Relationship between restr...
ralbida 2532 Formula-building rule for ...
rexbida 2533 Formula-building rule for ...
ralbidva 2534 Formula-building rule for ...
rexbidva 2535 Formula-building rule for ...
ralbid 2536 Formula-building rule for ...
rexbid 2537 Formula-building rule for ...
ralbidv 2538 Formula-building rule for ...
rexbidv 2539 Formula-building rule for ...
ralbidv2 2540 Formula-building rule for ...
rexbidv2 2541 Formula-building rule for ...
ralbii 2542 Inference adding restricte...
rexbii 2543 Inference adding restricte...
2ralbii 2544 Inference adding 2 restric...
2rexbii 2545 Inference adding 2 restric...
ralbii2 2546 Inference adding different...
rexbii2 2547 Inference adding different...
raleqbii 2548 Equality deduction for res...
rexeqbii 2549 Equality deduction for res...
ralbiia 2550 Inference adding restricte...
rexbiia 2551 Inference adding restricte...
2rexbiia 2552 Inference adding 2 restric...
r2alf 2553 Double restricted universa...
r2exf 2554 Double restricted existent...
r2al 2555 Double restricted universa...
r2ex 2556 Double restricted existent...
2ralbida 2557 Formula-building rule for ...
2ralbidva 2558 Formula-building rule for ...
2rexbidva 2559 Formula-building rule for ...
2ralbidv 2560 Formula-building rule for ...
2rexbidv 2561 Formula-building rule for ...
rexralbidv 2562 Formula-building rule for ...
ralinexa 2563 A transformation of restri...
rexanali 2564 A transformation of restri...
risset 2565 Two ways to say " ` A ` be...
hbral 2566 Bound-variable hypothesis ...
hbra1 2567 ` x ` is not free in ` A. ...
nfra1 2568 ` x ` is not free in ` A. ...
nfrald 2569 Deduction version of ~ nfr...
nfrexd 2570 Deduction version of ~ nfr...
nfral 2571 Bound-variable hypothesis ...
nfra2 2572 Similar to Lemma 24 of [Mo...
nfrex 2573 Bound-variable hypothesis ...
nfre1 2574 ` x ` is not free in ` E. ...
r3al 2575 Triple restricted universa...
alral 2576 Universal quantification i...
rexex 2577 Restricted existence impli...
ra4 2578 Restricted specialization....
ra4e 2579 Restricted specialization....
ra42 2580 Restricted specialization....
ra42e 2581 Restricted specialization....
rspec 2582 Specialization rule for re...
rgen 2583 Generalization rule for re...
rgen2a 2584 Generalization rule for re...
rgenw 2585 Generalization rule for re...
rgen2w 2586 Generalization rule for re...
mprg 2587 Modus ponens combined with...
mprgbir 2588 Modus ponens on biconditio...
ralim 2589 Distribution of restricted...
ralimi2 2590 Inference quantifying both...
ralimia 2591 Inference quantifying both...
ralimiaa 2592 Inference quantifying both...
ralimi 2593 Inference quantifying both...
ral2imi 2594 Inference quantifying ante...
ralimdaa 2595 Deduction quantifying both...
ralimdva 2596 Deduction quantifying both...
ralimdv 2597 Deduction quantifying both...
ralimdv2 2598 Inference quantifying both...
ralrimi 2599 Inference from Theorem 19....
ralrimiv 2600 Inference from Theorem 19....
ralrimiva 2601 Inference from Theorem 19....
ralrimivw 2602 Inference from Theorem 19....
r19.21t 2603 Theorem 19.21 of [Margaris...
r19.21 2604 Theorem 19.21 of [Margaris...
r19.21v 2605 Theorem 19.21 of [Margaris...
ralrimd 2606 Inference from Theorem 19....
ralrimdv 2607 Inference from Theorem 19....
ralrimdva 2608 Inference from Theorem 19....
ralrimivv 2609 Inference from Theorem 19....
ralrimivva 2610 Inference from Theorem 19....
ralrimivvva 2611 Inference from Theorem 19....
ralrimdvv 2612 Inference from Theorem 19....
ralrimdvva 2613 Inference from Theorem 19....
rgen2 2614 Generalization rule for re...
rgen3 2615 Generalization rule for re...
r19.21bi 2616 Inference from Theorem 19....
rspec2 2617 Specialization rule for re...
rspec3 2618 Specialization rule for re...
r19.21be 2619 Inference from Theorem 19....
nrex 2620 Inference adding restricte...
nrexdv 2621 Deduction adding restricte...
rexim 2622 Theorem 19.22 of [Margaris...
reximia 2623 Inference quantifying both...
reximi2 2624 Inference quantifying both...
reximi 2625 Inference quantifying both...
reximdai 2626 Deduction from Theorem 19....
reximdv2 2627 Deduction quantifying both...
reximdvai 2628 Deduction quantifying both...
reximdv 2629 Deduction from Theorem 19....
reximdva 2630 Deduction quantifying both...
r19.12 2631 Theorem 19.12 of [Margaris...
r19.23t 2632 Closed theorem form of ~ r...
r19.23 2633 Theorem 19.23 of [Margaris...
r19.23v 2634 Theorem 19.23 of [Margaris...
rexlimi 2635 Inference from Theorem 19....
rexlimiv 2636 Inference from Theorem 19....
rexlimiva 2637 Inference from Theorem 19....
rexlimivw 2638 Weaker version of ~ rexlim...
rexlimd 2639 Deduction from Theorem 19....
rexlimd2 2640 Version of ~ rexlimd with ...
rexlimdv 2641 Inference from Theorem 19....
rexlimdva 2642 Inference from Theorem 19....
rexlimdvaa 2643 Inference from Theorem 19....
rexlimdv3a 2644 Inference from Theorem 19....
rexlimdvw 2645 Inference from Theorem 19....
rexlimddv 2646 Restricted existential eli...
rexlimivv 2647 Inference from Theorem 19....
rexlimdvv 2648 Inference from Theorem 19....
rexlimdvva 2649 Inference from Theorem 19....
r19.26 2650 Theorem 19.26 of [Margaris...
r19.26-2 2651 Theorem 19.26 of [Margaris...
r19.26-3 2652 Theorem 19.26 of [Margaris...
r19.26m 2653 Theorem 19.26 of [Margaris...
ralbi 2654 Distribute a restricted un...
ralbiim 2655 Split a biconditional and ...
r19.27av 2656 Restricted version of one ...
r19.28av 2657 Restricted version of one ...
r19.29 2658 Theorem 19.29 of [Margaris...
r19.29r 2659 Variation of Theorem 19.29...
r19.30 2660 Theorem 19.30 of [Margaris...
r19.32v 2661 Theorem 19.32 of [Margaris...
r19.35 2662 Restricted quantifier vers...
r19.36av 2663 One direction of a restric...
r19.37 2664 Restricted version of one ...
r19.37av 2665 Restricted version of one ...
r19.40 2666 Restricted quantifier vers...
r19.41 2667 Restricted quantifier vers...
r19.41v 2668 Restricted quantifier vers...
r19.42v 2669 Restricted version of Theo...
r19.43 2670 Restricted version of Theo...
r19.44av 2671 One direction of a restric...
r19.45av 2672 Restricted version of one ...
ralcomf 2673 Commutation of restricted ...
rexcomf 2674 Commutation of restricted ...
ralcom 2675 Commutation of restricted ...
rexcom 2676 Commutation of restricted ...
rexcom13 2677 Swap 1st and 3rd restricte...
rexrot4 2678 Rotate existential restric...
ralcom2 2679 Commutation of restricted ...
ralcom3 2680 A commutative law for rest...
reean 2681 Rearrange existential quan...
reeanv 2682 Rearrange existential quan...
3reeanv 2683 Rearrange three existentia...
2ralor 2684 Distribute quantification ...
nfreu1 2685 ` x ` is not free in ` E! ...
nfrmo1 2686 ` x ` is not free in ` E* ...
nfreud 2687 Deduction version of ~ nfr...
nfrmod 2688 Deduction version of ~ nfr...
nfreu 2689 Bound-variable hypothesis ...
nfrmo 2690 Bound-variable hypothesis ...
rabid 2691 An "identity" law of concr...
rabid2 2692 An "identity" law for rest...
rabbi 2693 Equivalent wff's correspon...
rabswap 2694 Swap with a membership rel...
nfrab1 2695 The abstraction variable i...
nfrab 2696 A variable not free in a w...
reubida 2697 Formula-building rule for ...
reubidva 2698 Formula-building rule for ...
reubidv 2699 Formula-building rule for ...
reubiia 2700 Formula-building rule for ...
reubii 2701 Formula-building rule for ...
rmobida 2702 Formula-building rule for ...
rmobidva 2703 Formula-building rule for ...
rmobidv 2704 Formula-building rule for ...
rmobiia 2705 Formula-building rule for ...
rmobii 2706 Formula-building rule for ...
raleqf 2707 Equality theorem for restr...
rexeqf 2708 Equality theorem for restr...
reueq1f 2709 Equality theorem for restr...
rmoeq1f 2710 Equality theorem for restr...
raleq 2711 Equality theorem for restr...
rexeq 2712 Equality theorem for restr...
reueq1 2713 Equality theorem for restr...
rmoeq1 2714 Equality theorem for restr...
raleqi 2715 Equality inference for res...
rexeqi 2716 Equality inference for res...
raleqdv 2717 Equality deduction for res...
rexeqdv 2718 Equality deduction for res...
raleqbi1dv 2719 Equality deduction for res...
rexeqbi1dv 2720 Equality deduction for res...
reueqd 2721 Equality deduction for res...
rmoeqd 2722 Equality deduction for res...
raleqbidv 2723 Equality deduction for res...
rexeqbidv 2724 Equality deduction for res...
raleqbidva 2725 Equality deduction for res...
rexeqbidva 2726 Equality deduction for res...
mormo 2727 Unrestricted "at most one"...
reu5 2728 Restricted uniqueness in t...
reurex 2729 Restricted unique existenc...
reurmo 2730 Restricted existential uni...
rmo5 2731 Restricted "at most one" i...
nrexrmo 2732 Nonexistence implies restr...
cbvralf 2733 Rule used to change bound ...
cbvrexf 2734 Rule used to change bound ...
cbvral 2735 Rule used to change bound ...
cbvrex 2736 Rule used to change bound ...
cbvreu 2737 Change the bound variable ...
cbvrmo 2738 Change the bound variable ...
cbvralv 2739 Change the bound variable ...
cbvrexv 2740 Change the bound variable ...
cbvreuv 2741 Change the bound variable ...
cbvrmov 2742 Change the bound variable ...
cbvraldva2 2743 Rule used to change the bo...
cbvrexdva2 2744 Rule used to change the bo...
cbvraldva 2745 Rule used to change the bo...
cbvrexdva 2746 Rule used to change the bo...
cbvral2v 2747 Change bound variables of ...
cbvrex2v 2748 Change bound variables of ...
cbvral3v 2749 Change bound variables of ...
cbvralsv 2750 Change bound variable by u...
cbvrexsv 2751 Change bound variable by u...
sbralie 2752 Implicit to explicit subst...
rabbiia 2753 Equivalent wff's yield equ...
rabbidva 2754 Equivalent wff's yield equ...
rabbidv 2755 Equivalent wff's yield equ...
rabeqf 2756 Equality theorem for restr...
rabeq 2757 Equality theorem for restr...
rabeqbidv 2758 Equality of restricted cla...
rabeqbidva 2759 Equality of restricted cla...
rabeq2i 2760 Inference rule from equali...
cbvrab 2761 Rule to change the bound v...
cbvrabv 2762 Rule to change the bound v...
vjust 2764 Soundness justification th...
vex 2766 All set variables are sets...
isset 2767 Two ways to say " ` A ` is...
issetf 2768 A version of isset that do...
isseti 2769 A way to say " ` A ` is a ...
issetri 2770 A way to say " ` A ` is a ...
elex 2771 If a class is a member of ...
elexi 2772 If a class is a member of ...
elisset 2773 An element of a class exis...
elex22 2774 If two classes each contai...
elex2 2775 If a class contains anothe...
ralv 2776 A universal quantifier res...
rexv 2777 An existential quantifier ...
reuv 2778 A uniqueness quantifier re...
rmov 2779 A uniqueness quantifier re...
rabab 2780 A class abstraction restri...
ralcom4 2781 Commutation of restricted ...
rexcom4 2782 Commutation of restricted ...
rexcom4a 2783 Specialized existential co...
rexcom4b 2784 Specialized existential co...
ceqsalt 2785 Closed theorem version of ...
ceqsralt 2786 Restricted quantifier vers...
ceqsalg 2787 A representation of explic...
ceqsal 2788 A representation of explic...
ceqsalv 2789 A representation of explic...
ceqsralv 2790 Restricted quantifier vers...
gencl 2791 Implicit substitution for ...
2gencl 2792 Implicit substitution for ...
3gencl 2793 Implicit substitution for ...
cgsexg 2794 Implicit substitution infe...
cgsex2g 2795 Implicit substitution infe...
cgsex4g 2796 An implicit substitution i...
ceqsex 2797 Elimination of an existent...
ceqsexv 2798 Elimination of an existent...
ceqsex2 2799 Elimination of two existen...
ceqsex2v 2800 Elimination of two existen...
ceqsex3v 2801 Elimination of three exist...
ceqsex4v 2802 Elimination of four existe...
ceqsex6v 2803 Elimination of six existen...
ceqsex8v 2804 Elimination of eight exist...
gencbvex 2805 Change of bound variable u...
gencbvex2 2806 Restatement of ~ gencbvex ...
gencbval 2807 Change of bound variable u...
sbhypf 2808 Introduce an explicit subs...
vtoclgft 2809 Closed theorem form of ~ v...
vtocldf 2810 Implicit substitution of a...
vtocld 2811 Implicit substitution of a...
vtoclf 2812 Implicit substitution of a...
vtocl 2813 Implicit substitution of a...
vtocl2 2814 Implicit substitution of c...
vtocl3 2815 Implicit substitution of c...
vtoclb 2816 Implicit substitution of a...
vtoclgf 2817 Implicit substitution of a...
vtoclg 2818 Implicit substitution of a...
vtoclbg 2819 Implicit substitution of a...
vtocl2gf 2820 Implicit substitution of a...
vtocl3gf 2821 Implicit substitution of a...
vtocl2g 2822 Implicit substitution of 2...
vtoclgaf 2823 Implicit substitution of a...
vtoclga 2824 Implicit substitution of a...
vtocl2gaf 2825 Implicit substitution of 2...
vtocl2ga 2826 Implicit substitution of 2...
vtocl3gaf 2827 Implicit substitution of 3...
vtocl3ga 2828 Implicit substitution of 3...
vtocleg 2829 Implicit substitution of a...
vtoclegft 2830 Implicit substitution of a...
vtoclef 2831 Implicit substitution of a...
vtocle 2832 Implicit substitution of a...
vtoclri 2833 Implicit substitution of a...
cla4imgft 2834 A closed version of ~ cla4...
cla4gft 2835 A closed version of ~ cla4...
cla4imgf 2836 Rule of specialization, us...
cla4imegf 2837 Existential specialization...
cla4gf 2838 Rule of specialization, us...
cla4egf 2839 Existential specialization...
cla4imdv 2840 Restricted specialization,...
cla4dv 2841 Rule of specialization, us...
cla4imedv 2842 Restricted existential spe...
cla4gv 2843 Rule of specialization, us...
cla4egv 2844 Existential specialization...
cla42egv 2845 Existential specialization...
cla42gv 2846 Specialization with 2 quan...
cla43egv 2847 Existential specialization...
cla43gv 2848 Specialization with 3 quan...
cla4v 2849 Rule of specialization, us...
cla4ev 2850 Existential specialization...
cla42ev 2851 Existential specialization...
rcla4t 2852 A closed version of ~ rcla...
rcla4 2853 Restricted specialization,...
rcla4e 2854 Restricted existential spe...
rcla4v 2855 Restricted specialization,...
rcla4cv 2856 Restricted specialization,...
rcla4va 2857 Restricted specialization,...
rcla4cva 2858 Restricted specialization,...
rcla4ev 2859 Restricted existential spe...
rcla4imdv 2860 Restricted specialization,...
rcla4imedv 2861 Restricted existential spe...
rcla4dv 2862 Restricted specialization,...
rcla4edv 2863 Restricted existential spe...
rcla42 2864 2-variable restricted spec...
rcla42v 2865 2-variable restricted spec...
rcla42va 2866 2-variable restricted spec...
rcla42ev 2867 2-variable restricted exis...
rcla43v 2868 3-variable restricted spec...
rcla43ev 2869 3-variable restricted exis...
eqvinc 2870 A variable introduction la...
eqvincf 2871 A variable introduction la...
alexeq 2872 Two ways to express substi...
ceqex 2873 Equality implies equivalen...
ceqsexg 2874 A representation of explic...
ceqsexgv 2875 Elimination of an existent...
ceqsrexv 2876 Elimination of a restricte...
ceqsrexbv 2877 Elimination of a restricte...
ceqsrex2v 2878 Elimination of a restricte...
clel2 2879 An alternate definition of...
clel3g 2880 An alternate definition of...
clel3 2881 An alternate definition of...
clel4 2882 An alternate definition of...
pm13.183 2883 Compare theorem *13.183 in...
rr19.3v 2884 Restricted quantifier vers...
rr19.28v 2885 Restricted quantifier vers...
elabgt 2886 Membership in a class abst...
elabgf 2887 Membership in a class abst...
elabf 2888 Membership in a class abst...
elab 2889 Membership in a class abst...
elabg 2890 Membership in a class abst...
elab2g 2891 Membership in a class abst...
elab2 2892 Membership in a class abst...
elab4g 2893 Membership in a class abst...
elab3gf 2894 Membership in a class abst...
elab3g 2895 Membership in a class abst...
elab3 2896 Membership in a class abst...
elrabf 2897 Membership in a restricted...
elrab 2898 Membership in a restricted...
elrab3 2899 Membership in a restricted...
elrab2 2900 Membership in a class abst...
ralab 2901 Universal quantification o...
ralrab 2902 Universal quantification o...
rexab 2903 Existential quantification...
rexrab 2904 Existential quantification...
ralab2 2905 Universal quantification o...
ralrab2 2906 Universal quantification o...
rexab2 2907 Existential quantification...
rexrab2 2908 Existential quantification...
abidnf 2909 Identity used to create cl...
dedhb 2910 A deduction theorem for co...
eqeu 2911 A condition which implies ...
eueq 2912 Equality has existential u...
eueq1 2913 Equality has existential u...
eueq2 2914 Equality has existential u...
eueq3 2915 Equality has existential u...
moeq 2916 There is at most one set e...
moeq3 2917 "At most one" property of ...
mosub 2918 "At most one" remains true...
mo2icl 2919 Theorem for inferring "at ...
mob2 2920 Consequence of "at most on...
moi2 2921 Consequence of "at most on...
mob 2922 Equality implied by "at mo...
moi 2923 Equality implied by "at mo...
morex 2924 Derive membership from uni...
euxfr2 2925 Transfer existential uniqu...
euxfr 2926 Transfer existential uniqu...
euind 2927 Existential uniqueness via...
reu2 2928 A way to express restricte...
reu6 2929 A way to express restricte...
reu3 2930 A way to express restricte...
reu6i 2931 A condition which implies ...
eqreu 2932 A condition which implies ...
rmo4 2933 Restricted "at most one" u...
reu4 2934 Restricted uniqueness usin...
reu7 2935 Restricted uniqueness usin...
reu8 2936 Restricted uniqueness usin...
reueq 2937 Equality has existential u...
rmoan 2938 Restricted "at most one" s...
rmoim 2939 Restricted "at most one" i...
rmoimia 2940 Restricted "at most one" i...
rmoimi2 2941 Restricted "at most one" i...
2reuswap 2942 A condition allowing swap ...
reuind 2943 Existential uniqueness via...
2rmorex 2944 Double restricted quantifi...
2reu5lem1 2945 Lemma for ~ 2reu5 . Note ...
2reu5lem2 2946 Lemma for ~ 2reu5 . (Cont...
2reu5lem3 2947 Lemma for ~ 2reu5 . This ...
2reu5 2948 Double restricted existent...
cdeqi 2951 Deduce conditional equalit...
cdeqri 2952 Property of conditional eq...
cdeqth 2953 Deduce conditional equalit...
cdeqnot 2954 Distribute conditional equ...
cdeqal 2955 Distribute conditional equ...
cdeqab 2956 Distribute conditional equ...
cdeqal1 2957 Distribute conditional equ...
cdeqab1 2958 Distribute conditional equ...
cdeqim 2959 Distribute conditional equ...
cdeqcv 2960 Conditional equality for s...
cdeqeq 2961 Distribute conditional equ...
cdeqel 2962 Distribute conditional equ...
nfcdeq 2963 If we have a conditional e...
nfccdeq 2964 Variation of ~ nfcdeq for ...
ru 2965 Russell's Paradox. Propos...
dfsbcq 2968 This theorem, which is sim...
dfsbcq2 2969 This theorem, which is sim...
sbsbc 2970 Show that ~ df-sb and ~ df...
sbceq1d 2971 Equality theorem for class...
sbceq1dd 2972 Equality theorem for class...
sbc8g 2973 This is the closest we can...
sbc2or 2974 The disjunction of two equ...
sbcex 2975 By our definition of prope...
sbceq1a 2976 Equality theorem for class...
sbceq2a 2977 Equality theorem for class...
a4sbc 2978 Specialization: if a formu...
a4sbcd 2979 Specialization: if a formu...
sbcth 2980 A substitution into a theo...
sbcthdv 2981 Deduction version of ~ sbc...
sbcid 2982 An identity theorem for su...
nfsbc1d 2983 Deduction version of ~ nfs...
nfsbc1 2984 Bound-variable hypothesis ...
nfsbc1v 2985 Bound-variable hypothesis ...
nfsbcd 2986 Deduction version of ~ nfs...
nfsbc 2987 Bound-variable hypothesis ...
sbcco 2988 A composition law for clas...
sbcco2 2989 A composition law for clas...
sbc5 2990 An equivalence for class s...
sbc6g 2991 An equivalence for class s...
sbc6 2992 An equivalence for class s...
sbc7 2993 An equivalence for class s...
cbvsbc 2994 Change bound variables in ...
cbvsbcv 2995 Change the bound variable ...
sbciegft 2996 Conversion of implicit sub...
sbciegf 2997 Conversion of implicit sub...
sbcieg 2998 Conversion of implicit sub...
sbcie2g 2999 Conversion of implicit sub...
sbcie 3000 Conversion of implicit sub...
sbciedf 3001 Conversion of implicit sub...
sbcied 3002 Conversion of implicit sub...
sbcied2 3003 Conversion of implicit sub...
elrabsf 3004 Membership in a restricted...
eqsbc3 3005 Substitution applied to an...
sbcng 3006 Move negation in and out o...
sbcimg 3007 Distribution of class subs...
sbcan 3008 Distribution of class subs...
sbcang 3009 Distribution of class subs...
sbcor 3010 Distribution of class subs...
sbcorg 3011 Distribution of class subs...
sbcbig 3012 Distribution of class subs...
sbcal 3013 Move universal quantifier ...
sbcalg 3014 Move universal quantifier ...
sbcex2 3015 Move existential quantifie...
sbcexg 3016 Move existential quantifie...
sbceqal 3017 Set theory version of ~ sb...
sbeqalb 3018 Theorem *14.121 in [Whiteh...
sbcbid 3019 Formula-building deduction...
sbcbidv 3020 Formula-building deduction...
sbcbii 3021 Formula-building inference...
sbcbiiOLD 3022 Formula-building inference...
eqsbc3r 3023 ~ eqsbc3 with set variable...
sbc3ang 3024 Distribution of class subs...
sbcel1gv 3025 Class substitution into a ...
sbcel2gv 3026 Class substitution into a ...
sbcimdv 3027 Substitution analog of The...
sbctt 3028 Substitution for a variabl...
sbcgf 3029 Substitution for a variabl...
sbc19.21g 3030 Substitution for a variabl...
sbcg 3031 Substitution for a variabl...
sbc2iegf 3032 Conversion of implicit sub...
sbc2ie 3033 Conversion of implicit sub...
sbc2iedv 3034 Conversion of implicit sub...
sbc3ie 3035 Conversion of implicit sub...
sbccomlem 3036 Lemma for ~ sbccom . (Con...
sbccom 3037 Commutative law for double...
sbcralt 3038 Interchange class substitu...
sbcrext 3039 Interchange class substitu...
sbcralg 3040 Interchange class substitu...
sbcrexg 3041 Interchange class substitu...
sbcreug 3042 Interchange class substitu...
sbcabel 3043 Interchange class substitu...
ra4sbc 3044 Restricted quantifier vers...
ra4sbca 3045 Restricted quantifier vers...
ra4esbca 3046 Existence form of ~ ra4sbc...
a4esbc 3047 Existence form of ~ a4sbc ...
a4esbcd 3048 form of ~ a4sbc . (Contri...
sbcth2 3049 A substitution into a theo...
ra5 3050 Restricted quantifier vers...
rmo2 3051 Alternate definition of re...
rmo2i 3052 Condition implying restric...
rmo3 3053 Restricted "at most one" u...
rmob 3054 Consequence of "at most on...
rmoi 3055 Consequence of "at most on...
csb2 3058 Alternate expression for t...
csbeq1 3059 Analog of ~ dfsbcq for pro...
cbvcsb 3060 Change bound variables in ...
cbvcsbv 3061 Change the bound variable ...
csbeq1d 3062 Equality deduction for pro...
csbid 3063 Analog of ~ sbid for prope...
csbeq1a 3064 Equality theorem for prope...
csbco 3065 Composition law for chaine...
csbexg 3066 The existence of proper su...
csbex 3067 The existence of proper su...
csbtt 3068 Substitution doesn't affec...
csbconstgf 3069 Substitution doesn't affec...
csbconstg 3070 Substitution doesn't affec...
sbcel12g 3071 Distribute proper substitu...
sbceqg 3072 Distribute proper substitu...
sbcnel12g 3073 Distribute proper substitu...
sbcne12g 3074 Distribute proper substitu...
sbcel1g 3075 Move proper substitution i...
sbceq1g 3076 Move proper substitution t...
sbcel2g 3077 Move proper substitution i...
sbceq2g 3078 Move proper substitution t...
csbcomg 3079 Commutative law for double...
csbeq2d 3080 Formula-building deduction...
csbeq2dv 3081 Formula-building deduction...
csbeq2i 3082 Formula-building inference...
csbvarg 3083 The proper substitution of...
sbccsbg 3084 Substitution into a wff ex...
sbccsb2g 3085 Substitution into a wff ex...
nfcsb1d 3086 Bound-variable hypothesis ...
nfcsb1 3087 Bound-variable hypothesis ...
nfcsb1v 3088 Bound-variable hypothesis ...
nfcsbd 3089 Deduction version of ~ nfc...
nfcsb 3090 Bound-variable hypothesis ...
csbhypf 3091 Introduce an explicit subs...
csbiebt 3092 Conversion of implicit sub...
csbiedf 3093 Conversion of implicit sub...
csbieb 3094 Bidirectional conversion b...
csbiebg 3095 Bidirectional conversion b...
csbiegf 3096 Conversion of implicit sub...
csbief 3097 Conversion of implicit sub...
csbied 3098 Conversion of implicit sub...
csbied2 3099 Conversion of implicit sub...
csbie2t 3100 Conversion of implicit sub...
csbie2 3101 Conversion of implicit sub...
csbie2g 3102 Conversion of implicit sub...
sbcnestgf 3103 Nest the composition of tw...
csbnestgf 3104 Nest the composition of tw...
sbcnestg 3105 Nest the composition of tw...
csbnestg 3106 Nest the composition of tw...
csbnestgOLD 3107 Nest the composition of tw...
csbnest1g 3108 Nest the composition of tw...
csbnest1gOLD 3109 Nest the composition of tw...
csbidmg 3110 Idempotent law for class s...
sbcco3g 3111 Composition of two substit...
sbcco3gOLD 3112 Composition of two substit...
csbco3g 3113 Composition of two class s...
csbco3gOLD 3114 Composition of two class s...
ra4csbela 3115 Special case related to ~ ...
sbnfc2 3116 Two ways of expressing " `...
csbabg 3117 Move substitution into a c...
cbvralcsf 3118 A more general version of ...
cbvrexcsf 3119 A more general version of ...
cbvreucsf 3120 A more general version of ...
cbvrabcsf 3121 A more general version of ...
cbvralv2 3122 Rule used to change the bo...
cbvrexv2 3123 Rule used to change the bo...
difjust 3129 Soundness justification th...
unjust 3131 Soundness justification th...
injust 3133 Soundness justification th...
dfin5 3135 Alternate definition for t...
dfdif2 3136 Alternate definition of cl...
eldif 3137 Expansion of membership in...
eldifd 3138 If a class is in one class...
eldifad 3139 If a class is in the diffe...
eldifbd 3140 If a class is in the diffe...
dfss 3142 Variant of subclass defini...
dfss2 3144 Alternate definition of th...
dfss3 3145 Alternate definition of su...
dfss2f 3146 Equivalence for subclass r...
dfss3f 3147 Equivalence for subclass r...
nfss 3148 If ` x ` is not free in ` ...
ssel 3149 Membership relationships f...
ssel2 3150 Membership relationships f...
sseli 3151 Membership inference from ...
sselii 3152 Membership inference from ...
sseldi 3153 Membership inference from ...
sseld 3154 Membership deduction from ...
sselda 3155 Membership deduction from ...
sseldd 3156 Membership inference from ...
ssneld 3157 If a class is not in anoth...
ssneldd 3158 If an element is not in a ...
ssriv 3159 Inference rule based on su...
ssrdv 3160 Deduction rule based on su...
sstr2 3161 Transitivity of subclasses...
sstr 3162 Transitivity of subclasses...
sstri 3163 Subclass transitivity infe...
sstrd 3164 Subclass transitivity dedu...
syl5ss 3165 Subclass transitivity dedu...
syl6ss 3166 Subclass transitivity dedu...
sylan9ss 3167 A subclass transitivity de...
sylan9ssr 3168 A subclass transitivity de...
eqss 3169 The subclass relationship ...
eqssi 3170 Infer equality from two su...
eqssd 3171 Equality deduction from tw...
ssid 3172 Any class is a subclass of...
ssv 3173 Any class is a subclass of...
sseq1 3174 Equality theorem for subcl...
sseq2 3175 Equality theorem for the s...
sseq12 3176 Equality theorem for the s...
sseq1i 3177 An equality inference for ...
sseq2i 3178 An equality inference for ...
sseq12i 3179 An equality inference for ...
sseq1d 3180 An equality deduction for ...
sseq2d 3181 An equality deduction for ...
sseq12d 3182 An equality deduction for ...
eqsstri 3183 Substitution of equality i...
eqsstr3i 3184 Substitution of equality i...
sseqtri 3185 Substitution of equality i...
sseqtr4i 3186 Substitution of equality i...
eqsstrd 3187 Substitution of equality i...
eqsstr3d 3188 Substitution of equality i...
sseqtrd 3189 Substitution of equality i...
sseqtr4d 3190 Substitution of equality i...
3sstr3i 3191 Substitution of equality i...
3sstr4i 3192 Substitution of equality i...
3sstr3g 3193 Substitution of equality i...
3sstr4g 3194 Substitution of equality i...
3sstr3d 3195 Substitution of equality i...
3sstr4d 3196 Substitution of equality i...
syl5eqss 3197 B chained subclass and equ...
syl5eqssr 3198 B chained subclass and equ...
syl6sseq 3199 A chained subclass and equ...
syl6sseqr 3200 A chained subclass and equ...
syl5sseq 3201 Subclass transitivity dedu...
syl5sseqr 3202 Subclass transitivity dedu...
syl6eqss 3203 A chained subclass and equ...
syl6eqssr 3204 A chained subclass and equ...
eqimss 3205 Equality implies the subcl...
eqimss2 3206 Equality implies the subcl...
eqimssi 3207 Infer subclass relationshi...
eqimss2i 3208 Infer subclass relationshi...
nssne1 3209 Two classes are different ...
nssne2 3210 Two classes are different ...
nss 3211 Negation of subclass relat...
ssralv 3212 Quantification restricted ...
ssrexv 3213 Existential quantification...
ralss 3214 Restricted universal quant...
rexss 3215 Restricted existential qua...
ss2ab 3216 Class abstractions in a su...
abss 3217 Class abstraction in a sub...
ssab 3218 Subclass of a class abstra...
ssabral 3219 The relation for a subclas...
ss2abi 3220 Inference of abstraction s...
ss2abdv 3221 Deduction of abstraction s...
abssdv 3222 Deduction of abstraction s...
abssi 3223 Inference of abstraction s...
ss2rab 3224 Restricted abstraction cla...
rabss 3225 Restricted class abstracti...
ssrab 3226 Subclass of a restricted c...
ssrabdv 3227 Subclass of a restricted c...
rabssdv 3228 Subclass of a restricted c...
ss2rabdv 3229 Deduction of restricted ab...
ss2rabi 3230 Inference of restricted ab...
rabss2 3231 Subclass law for restricte...
ssab2 3232 Subclass relation for the ...
ssrab2 3233 Subclass relation for a re...
rabssab 3234 A restricted class is a su...
uniiunlem 3235 A subset relationship usef...
dfpss2 3236 Alternate definition of pr...
dfpss3 3237 Alternate definition of pr...
psseq1 3238 Equality theorem for prope...
psseq2 3239 Equality theorem for prope...
psseq1i 3240 An equality inference for ...
psseq2i 3241 An equality inference for ...
psseq12i 3242 An equality inference for ...
psseq1d 3243 An equality deduction for ...
psseq2d 3244 An equality deduction for ...
psseq12d 3245 An equality deduction for ...
pssss 3246 A proper subclass is a sub...
pssne 3247 Two classes in a proper su...
pssssd 3248 Deduce subclass from prope...
pssned 3249 Proper subclasses are uneq...
sspss 3250 Subclass in terms of prope...
pssirr 3251 Proper subclass is irrefle...
pssn2lp 3252 Proper subclass has no 2-c...
sspsstri 3253 Two ways of stating tricho...
ssnpss 3254 Partial trichotomy law for...
psstr 3255 Transitive law for proper ...
sspsstr 3256 Transitive law for subclas...
psssstr 3257 Transitive law for subclas...
psstrd 3258 Proper subclass inclusion ...
sspsstrd 3259 Transitivity involving sub...
psssstrd 3260 Transitivity involving sub...
npss 3261 A class is not a proper su...
difeq1 3262 Equality theorem for class...
difeq2 3263 Equality theorem for class...
difeq12 3264 Equality theorem for class...
difeq1i 3265 Inference adding differenc...
difeq2i 3266 Inference adding differenc...
difeq12i 3267 Equality inference for cla...
difeq1d 3268 Deduction adding differenc...
difeq2d 3269 Deduction adding differenc...
difeq12d 3270 Equality deduction for cla...
difeqri 3271 Inference from membership ...
nfdif 3272 Bound-variable hypothesis ...
eldifi 3273 Implication of membership ...
eldifn 3274 Implication of membership ...
elndif 3275 A set does not belong to a...
neldif 3276 Implication of membership ...
difdif 3277 Double class difference. ...
difss 3278 Subclass relationship for ...
difssd 3279 A difference of two classe...
difss2 3280 If a class is contained in...
difss2d 3281 If a class is contained in...
ssdifss 3282 Preservation of a subclass...
ddif 3283 Double complement under un...
ssconb 3284 Contraposition law for sub...
sscon 3285 Contraposition law for sub...
ssdif 3286 Difference law for subsets...
ssdifd 3287 If ` A ` is contained in `...
sscond 3288 If ` A ` is contained in `...
ssdifssd 3289 If ` A ` is contained in `...
ssdif2d 3290 If ` A ` is contained in `...
elun 3291 Expansion of membership in...
uneqri 3292 Inference from membership ...
unidm 3293 Idempotent law for union o...
uncom 3294 Commutative law for union ...
equncom 3295 If a class equals the unio...
equncomi 3296 Inference form of ~ equnco...
uneq1 3297 Equality theorem for union...
uneq2 3298 Equality theorem for the u...
uneq12 3299 Equality theorem for union...
uneq1i 3300 Inference adding union to ...
uneq2i 3301 Inference adding union to ...
uneq12i 3302 Equality inference for uni...
uneq1d 3303 Deduction adding union to ...
uneq2d 3304 Deduction adding union to ...
uneq12d 3305 Equality deduction for uni...
nfun 3306 Bound-variable hypothesis ...
unass 3307 Associative law for union ...
un12 3308 A rearrangement of union. ...
un23 3309 A rearrangement of union. ...
un4 3310 A rearrangement of the uni...
unundi 3311 Union distributes over its...
unundir 3312 Union distributes over its...
ssun1 3313 Subclass relationship for ...
ssun2 3314 Subclass relationship for ...
ssun3 3315 Subclass law for union of ...
ssun4 3316 Subclass law for union of ...
elun1 3317 Membership law for union o...
elun2 3318 Membership law for union o...
unss1 3319 Subclass law for union of ...
ssequn1 3320 A relationship between sub...
unss2 3321 Subclass law for union of ...
unss12 3322 Subclass law for union of ...
ssequn2 3323 A relationship between sub...
unss 3324 The union of two subclasse...
unssi 3325 An inference showing the u...
unssd 3326 A deduction showing the un...
unssad 3327 If ` ( A u. B ) ` is conta...
unssbd 3328 If ` ( A u. B ) ` is conta...
ssun 3329 A condition that implies i...
rexun 3330 Restricted existential qua...
ralunb 3331 Restricted quantification ...
ralun 3332 Restricted quantification ...
elin 3333 Expansion of membership in...
elin2 3334 Membership in a class defi...
elin3 3335 Membership in a class defi...
incom 3336 Commutative law for inters...
ineqri 3337 Inference from membership ...
ineq1 3338 Equality theorem for inter...
ineq2 3339 Equality theorem for inter...
ineq12 3340 Equality theorem for inter...
ineq1i 3341 Equality inference for int...
ineq2i 3342 Equality inference for int...
ineq12i 3343 Equality inference for int...
ineq1d 3344 Equality deduction for int...
ineq2d 3345 Equality deduction for int...
ineq12d 3346 Equality deduction for int...
ineqan12d 3347 Equality deduction for int...
dfss1 3348 A frequently-used variant ...
dfss5 3349 Another definition of subc...
nfin 3350 Bound-variable hypothesis ...
csbing 3351 Distribute proper substitu...
rabbi2dva 3352 Deduction from a wff to a ...
inidm 3353 Idempotent law for interse...
inass 3354 Associative law for inters...
in12 3355 A rearrangement of interse...
in32 3356 A rearrangement of interse...
in13 3357 A rearrangement of interse...
in31 3358 A rearrangement of interse...
inrot 3359 Rotate the intersection of...
in4 3360 Rearrangement of intersect...
inindi 3361 Intersection distributes o...
inindir 3362 Intersection distributes o...
sseqin2 3363 A relationship between sub...
inss1 3364 The intersection of two cl...
inss2 3365 The intersection of two cl...
ssin 3366 Subclass of intersection. ...
ssini 3367 An inference showing that ...
ssind 3368 A deduction showing that t...
ssrin 3369 Add right intersection to ...
sslin 3370 Add left intersection to s...
ss2in 3371 Intersection of subclasses...
ssinss1 3372 Intersection preserves sub...
inss 3373 Inclusion of an intersecti...
unabs 3374 Absorption law for union. ...
inabs 3375 Absorption law for interse...
nssinpss 3376 Negation of subclass expre...
nsspssun 3377 Negation of subclass expre...
dfss4 3378 Subclass defined in terms ...
dfun2 3379 An alternate definition of...
dfin2 3380 An alternate definition of...
difin 3381 Difference with intersecti...
dfun3 3382 Union defined in terms of ...
dfin3 3383 Intersection defined in te...
dfin4 3384 Alternate definition of th...
invdif 3385 Intersection with universa...
indif 3386 Intersection with class di...
indif2 3387 Bring an intersection in a...
indif1 3388 Bring an intersection in a...
indifcom 3389 Commutation law for inters...
indi 3390 Distributive law for inter...
undi 3391 Distributive law for union...
indir 3392 Distributive law for inter...
undir 3393 Distributive law for union...
unineq 3394 Infer equality from equali...
uneqin 3395 Equality of union and inte...
difundi 3396 Distributive law for class...
difundir 3397 Distributive law for class...
difindi 3398 Distributive law for class...
difindir 3399 Distributive law for class...
indifdir 3400 Distribute intersection ov...
undm 3401 DeMorgan's law for union. ...
indm 3402 DeMorgan's law for interse...
difun1 3403 A relationship involving d...
undif3 3404 An equality involving clas...
difin2 3405 Represent a set difference...
dif32 3406 Swap second and third argu...
difabs 3407 Absorption-like law for cl...
symdif1 3408 Two ways to express symmet...
symdif2 3409 Two ways to express symmet...
unab 3410 Union of two class abstrac...
inab 3411 Intersection of two class ...
difab 3412 Difference of two class ab...
notab 3413 A class builder defined by...
unrab 3414 Union of two restricted cl...
inrab 3415 Intersection of two restri...
inrab2 3416 Intersection with a restri...
difrab 3417 Difference of two restrict...
dfrab2 3418 Alternate definition of re...
dfrab3 3419 Alternate definition of re...
notrab 3420 Complementation of a restr...
dfrab3ss 3421 Restricted class abstracti...
rabun2 3422 Abstraction restricted to ...
reuss2 3423 Transfer uniqueness to a s...
reuss 3424 Transfer uniqueness to a s...
reuun1 3425 Transfer uniqueness to a s...
reuun2 3426 Transfer uniqueness to a s...
reupick 3427 Restricted uniqueness "pic...
reupick3 3428 Restricted uniqueness "pic...
reupick2 3429 Restricted uniqueness "pic...
dfnul2 3432 Alternate definition of th...
dfnul3 3433 Alternate definition of th...
noel 3434 The empty set has no eleme...
n0i 3435 If a set has elements, it ...
ne0i 3436 If a set has elements, it ...
vn0 3437 The universal class is not...
n0f 3438 A nonempty class has at le...
n0 3439 A nonempty class has at le...
neq0 3440 A nonempty class has at le...
reximdva0 3441 Restricted existence deduc...
n0moeu 3442 A case of equivalence of "...
rex0 3443 Vacuous existential quanti...
eq0 3444 The empty set has no eleme...
eqv 3445 The universe contains ever...
0el 3446 Membership of the empty se...
abvor0 3447 The class builder of a wff...
abn0 3448 Nonempty class abstraction...
rabn0 3449 Non-empty restricted class...
rab0 3450 Any restricted class abstr...
rabeq0 3451 Condition for a restricted...
rabxm 3452 Law of excluded middle, in...
rabnc 3453 Law of noncontradiction, i...
un0 3454 The union of a class with ...
in0 3455 The intersection of a clas...
inv1 3456 The intersection of a clas...
unv 3457 The union of a class with ...
0ss 3458 The null set is a subset o...
ss0b 3459 Any subset of the empty se...
ss0 3460 Any subset of the empty se...
sseq0 3461 A subclass of an empty cla...
ssn0 3462 A class with a nonempty su...
abf 3463 A class builder with a fal...
eq0rdv 3464 Deduction rule for equalit...
un00 3465 Two classes are empty iff ...
vss 3466 Only the universal class h...
0pss 3467 The null set is a proper s...
npss0 3468 No set is a proper subset ...
pssv 3469 Any non-universal class is...
disj 3470 Two ways of saying that tw...
disjr 3471 Two ways of saying that tw...
disj1 3472 Two ways of saying that tw...
reldisj 3473 Two ways of saying that tw...
disj3 3474 Two ways of saying that tw...
disjne 3475 Members of disjoint sets a...
disjel 3476 A set can't belong to both...
disj2 3477 Two ways of saying that tw...
disj4 3478 Two ways of saying that tw...
ssdisj 3479 Intersection with a subcla...
disjpss 3480 A class is a proper subset...
undisj1 3481 The union of disjoint clas...
undisj2 3482 The union of disjoint clas...
ssindif0 3483 Subclass expressed in term...
inelcm 3484 The intersection of classe...
minel 3485 A minimum element of a cla...
undif4 3486 Distribute union over diff...
disjssun 3487 Subset relation for disjoi...
ssdif0 3488 Subclass expressed in term...
vdif0 3489 Universal class equality i...
pssdifn0 3490 A proper subclass has a no...
pssdif 3491 A proper subclass has a no...
ssnelpss 3492 A subclass missing a membe...
ssnelpssd 3493 Subclass inclusion with on...
pssnel 3494 A proper subclass has a me...
difin0ss 3495 Difference, intersection, ...
inssdif0 3496 Intersection, subclass, an...
difid 3497 The difference between a c...
difidALT 3498 The difference between a c...
dif0 3499 The difference between a c...
0dif 3500 The difference between the...
disjdif 3501 A class and its relative c...
difin0 3502 The difference of a class ...
undifv 3503 The union of a class and i...
undif1 3504 Absorption of difference b...
undif2 3505 Absorption of difference b...
undifabs 3506 Absorption of difference b...
inundif 3507 The intersection and class...
difun2 3508 Absorption of union by dif...
undif 3509 Union of complementary par...
ssdifin0 3510 A subset of a difference d...
ssdifeq0 3511 A class is a subclass of i...
ssundif 3512 A condition equivalent to ...
difcom 3513 Swap the arguments of a cl...
pssdifcom1 3514 Two ways to express overla...
pssdifcom2 3515 Two ways to express non-co...
difdifdir 3516 Distributive law for class...
uneqdifeq 3517 Two ways to say that ` A `...
r19.2z 3518 Theorem 19.2 of [Margaris]...
r19.2zb 3519 A response to the notion t...
r19.3rz 3520 Restricted quantification ...
r19.28z 3521 Restricted quantifier vers...
r19.3rzv 3522 Restricted quantification ...
r19.9rzv 3523 Restricted quantification ...
r19.28zv 3524 Restricted quantifier vers...
r19.37zv 3525 Restricted quantifier vers...
r19.45zv 3526 Restricted version of Theo...
r19.27z 3527 Restricted quantifier vers...
r19.27zv 3528 Restricted quantifier vers...
r19.36zv 3529 Restricted quantifier vers...
rzal 3530 Vacuous quantification is ...
rexn0 3531 Restricted existential qua...
ralidm 3532 Idempotent law for restric...
ral0 3533 Vacuous universal quantifi...
rgenz 3534 Generalization rule that e...
ralf0 3535 The quantification of a fa...
raaan 3536 Rearrange restricted quant...
raaanv 3537 Rearrange restricted quant...
sbss 3538 Set substitution into the ...
dfif2 3541 An alternate definition of...
dfif6 3542 An alternate definition of...
ifeq1 3543 Equality theorem for condi...
ifeq2 3544 Equality theorem for condi...
iftrue 3545 Value of the conditional o...
iffalse 3546 Value of the conditional o...
ifnefalse 3547 When values are unequal, b...
ifsb 3548 Distribute a function over...
dfif3 3549 Alternate definition of th...
dfif4 3550 Alternate definition of th...
dfif5 3551 Alternate definition of th...
ifeq12 3552 Equality theorem for condi...
ifeq1d 3553 Equality deduction for con...
ifeq2d 3554 Equality deduction for con...
ifeq12d 3555 Equality deduction for con...
ifbi 3556 Equivalence theorem for co...
ifbid 3557 Equivalence deduction for ...
ifbieq2i 3558 Equivalence/equality infer...
ifbieq2d 3559 Equivalence/equality deduc...
ifbieq12i 3560 Equivalence deduction for ...
ifbieq12d 3561 Equivalence deduction for ...
nfifd 3562 Deduction version of ~ nfi...
nfif 3563 Bound-variable hypothesis ...
ifeq1da 3564 Conditional equality. (Co...
ifeq2da 3565 Conditional equality. (Co...
ifclda 3566 Conditional closure. (Con...
csbifg 3567 Distribute proper substitu...
elimif 3568 Elimination of a condition...
ifbothda 3569 A wff ` th ` containing a ...
ifboth 3570 A wff ` th ` containing a ...
ifid 3571 Identical true and false a...
eqif 3572 Expansion of an equality w...
elif 3573 Membership in a conditiona...
ifel 3574 Membership of a conditiona...
ifcl 3575 Membership (closure) of a ...
ifeqor 3576 The possible values of a c...
ifnot 3577 Negating the first argumen...
ifan 3578 Rewrite a conjunction in a...
ifor 3579 Rewrite a disjunction in a...
dedth 3580 Weak deduction theorem tha...
dedth2h 3581 Weak deduction theorem eli...
dedth3h 3582 Weak deduction theorem eli...
dedth4h 3583 Weak deduction theorem eli...
dedth2v 3584 Weak deduction theorem for...
dedth3v 3585 Weak deduction theorem for...
dedth4v 3586 Weak deduction theorem for...
elimhyp 3587 Eliminate a hypothesis con...
elimhyp2v 3588 Eliminate a hypothesis con...
elimhyp3v 3589 Eliminate a hypothesis con...
elimhyp4v 3590 Eliminate a hypothesis con...
elimel 3591 Eliminate a membership hyp...
elimdhyp 3592 Version of ~ elimhyp where...
keephyp 3593 Transform a hypothesis ` p...
keephyp2v 3594 Keep a hypothesis containi...
keephyp3v 3595 Keep a hypothesis containi...
keepel 3596 Keep a membership hypothes...
ifex 3597 Conditional operator exist...
ifexg 3598 Conditional operator exist...
pwjust 3600 Soundness justification th...
pweq 3602 Equality theorem for power...
pweqi 3603 Equality inference for pow...
pweqd 3604 Equality deduction for pow...
elpw 3605 Membership in a power clas...
elpwg 3606 Membership in a power clas...
elpwi 3607 Subset relation implied by...
elpwid 3608 An element of a power clas...
elelpwi 3609 If ` A ` belongs to a part...
nfpw 3610 Bound-variable hypothesis ...
pwidg 3611 Membership of the original...
pwid 3612 A set is a member of its p...
pwss 3613 Subclass relationship for ...
snjust 3619 Soundness justification th...
sneq 3625 Equality theorem for singl...
sneqi 3626 Equality inference for sin...
sneqd 3627 Equality deduction for sin...
dfsn2 3628 Alternate definition of si...
elsn 3629 There is only one element ...
dfpr2 3630 Alternate definition of un...
elprg 3631 A member of an unordered p...
elpr 3632 A member of an unordered p...
elpr2 3633 A member of an unordered p...
elpri 3634 If a class is an element o...
nelpri 3635 If an element doesn't matc...
elsncg 3636 There is only one element ...
elsnc 3637 There is only one element ...
elsni 3638 There is only one element ...
snidg 3639 A set is a member of its s...
snidb 3640 A class is a set iff it is...
snid 3641 A set is a member of its s...
elsnc2g 3642 There is only one element ...
elsnc2 3643 There is only one element ...
ralsns 3644 Substitution expressed in ...
rexsns 3645 Restricted existential qua...
ralsng 3646 Substitution expressed in ...
rexsng 3647 Restricted existential qua...
ralsn 3648 Convert a quantification o...
rexsn 3649 Restricted existential qua...
eltpg 3650 Members of an unordered tr...
eltpi 3651 A member of an unordered t...
eltp 3652 A member of an unordered t...
dftp2 3653 Alternate definition of un...
nfpr 3654 Bound-variable hypothesis ...
ifpr 3655 Membership of a conditiona...
ralprg 3656 Convert a quantification o...
rexprg 3657 Convert a quantification o...
raltpg 3658 Convert a quantification o...
rextpg 3659 Convert a quantification o...
ralpr 3660 Convert a quantification o...
rexpr 3661 Convert an existential qua...
raltp 3662 Convert a quantification o...
rextp 3663 Convert a quantification o...
sbcsng 3664 Substitution expressed in ...
nfsn 3665 Bound-variable hypothesis ...
csbsng 3666 Distribute proper substitu...
disjsn 3667 Intersection with the sing...
disjsn2 3668 Intersection of distinct s...
snprc 3669 The singleton of a proper ...
r19.12sn 3670 Special case of ~ r19.12 w...
rabsn 3671 Condition where a restrict...
euabsn2 3672 Another way to express exi...
euabsn 3673 Another way to express exi...
reusn 3674 A way to express restricte...
absneu 3675 Restricted existential uni...
rabsneu 3676 Restricted existential uni...
eusn 3677 Two ways to express " ` A ...
rabsnt 3678 Truth implied by equality ...
prcom 3679 Commutative law for unorde...
preq1 3680 Equality theorem for unord...
preq2 3681 Equality theorem for unord...
preq12 3682 Equality theorem for unord...
preq1i 3683 Equality inference for uno...
preq2i 3684 Equality inference for uno...
preq12i 3685 Equality inference for uno...
preq1d 3686 Equality deduction for uno...
preq2d 3687 Equality deduction for uno...
preq12d 3688 Equality deduction for uno...
tpeq1 3689 Equality theorem for unord...
tpeq2 3690 Equality theorem for unord...
tpeq3 3691 Equality theorem for unord...
tpeq1d 3692 Equality theorem for unord...
tpeq2d 3693 Equality theorem for unord...
tpeq3d 3694 Equality theorem for unord...
tpeq123d 3695 Equality theorem for unord...
tprot 3696 Rotation of the elements o...
tpcoma 3697 Swap 1st and 2nd members o...
tpcomb 3698 Swap 2nd and 3rd members o...
tpass 3699 Split off the first elemen...
qdass 3700 Two ways to write an unord...
qdassr 3701 Two ways to write an unord...
tpidm12 3702 Unordered triple ` { A , A...
tpidm13 3703 Unordered triple ` { A , B...
tpidm23 3704 Unordered triple ` { A , B...
tpidm 3705 Unordered triple ` { A , A...
prid1g 3706 An unordered pair contains...
prid2g 3707 An unordered pair contains...
prid1 3708 An unordered pair contains...
prid2 3709 An unordered pair contains...
prprc1 3710 A proper class vanishes in...
prprc2 3711 A proper class vanishes in...
prprc 3712 An unordered pair containi...
tpid1 3713 One of the three elements ...
tpid2 3714 One of the three elements ...
tpid3g 3715 Closed theorem form of ~ t...
tpid3 3716 One of the three elements ...
snnzg 3717 The singleton of a set is ...
snnz 3718 The singleton of a set is ...
prnz 3719 A pair containing a set is...
prnzg 3720 A pair containing a set is...
tpnz 3721 A triplet containing a set...
snss 3722 The singleton of an elemen...
eldifsn 3723 Membership in a set with a...
eldifsni 3724 Membership in a set with a...
neldifsn 3725 ` A ` is not in ` ( B \ { ...
neldifsnd 3726 ` A ` is not in ` ( B \ { ...
rexdifsn 3727 Restricted existential qua...
snssg 3728 The singleton of an elemen...
difsn 3729 An element not in a set ca...
difprsn 3730 Removal of a singleton fro...
difsneq 3731 ` ( B \ { A } ) ` equals `...
difsnpss 3732 ` ( B \ { A } ) ` is a pro...
snssi 3733 The singleton of an elemen...
snssd 3734 The singleton of an elemen...
difsnid 3735 If we remove a single elem...
pw0 3736 Compute the power set of t...
pwpw0 3737 Compute the power set of t...
snsspr1 3738 A singleton is a subset of...
snsspr2 3739 A singleton is a subset of...
snsstp1 3740 A singleton is a subset of...
snsstp2 3741 A singleton is a subset of...
snsstp3 3742 A singleton is a subset of...
prss 3743 A pair of elements of a cl...
prssg 3744 A pair of elements of a cl...
prssi 3745 A pair of elements of a cl...
sssn 3746 The subsets of a singleton...
ssunsn2 3747 The property of being sand...
ssunsn 3748 Possible values for a set ...
eqsn 3749 Two ways to express that a...
ssunpr 3750 Possible values for a set ...
sspr 3751 The subsets of a pair. (C...
sstp 3752 The subsets of a triple. ...
tpss 3753 A triplet of elements of a...
sneqr 3754 If the singletons of two s...
snsssn 3755 If a singleton is a subset...
sneqrg 3756 Closed form of ~ sneqr . ...
sneqbg 3757 Two singletons of sets are...
snsspw 3758 The singleton of a class i...
prsspw 3759 An unordered pair belongs ...
preqr1 3760 Reverse equality lemma for...
preqr2 3761 Reverse equality lemma for...
preq12b 3762 Equality relationship for ...
prel12 3763 Equality of two unordered ...
opthpr 3764 A way to represent ordered...
preq12bg 3765 Closed form of ~ preq12b ....
preqsn 3766 Equivalence for a pair equ...
dfopif 3767 Rewrite ~ df-op using ` if...
dfopg 3768 Value of the ordered pair ...
dfop 3769 Value of an ordered pair w...
opeq1 3770 Equality theorem for order...
opeq2 3771 Equality theorem for order...
opeq12 3772 Equality theorem for order...
opeq1i 3773 Equality inference for ord...
opeq2i 3774 Equality inference for ord...
opeq12i 3775 Equality inference for ord...
opeq1d 3776 Equality deduction for ord...
opeq2d 3777 Equality deduction for ord...
opeq12d 3778 Equality deduction for ord...
oteq1 3779 Equality theorem for order...
oteq2 3780 Equality theorem for order...
oteq3 3781 Equality theorem for order...
oteq1d 3782 Equality deduction for ord...
oteq2d 3783 Equality deduction for ord...
oteq3d 3784 Equality deduction for ord...
oteq123d 3785 Equality deduction for ord...
nfop 3786 Bound-variable hypothesis ...
nfopd 3787 Deduction version of bound...
opid 3788 The ordered pair ` <. A , ...
ralunsn 3789 Restricted quantification ...
2ralunsn 3790 Double restricted quantifi...
opprc 3791 Expansion of an ordered pa...
opprc1 3792 Expansion of an ordered pa...
opprc2 3793 Expansion of an ordered pa...
oprcl 3794 If an ordered pair has an ...
pwsn 3795 The power set of a singlet...
pwsnALT 3796 The power set of a singlet...
pwpr 3797 The power set of an unorde...
pwtp 3798 The power set of an unorde...
pwpwpw0 3799 Compute the power set of t...
pwv 3800 The power class of the uni...
dfuni2 3803 Alternate definition of cl...
eluni 3804 Membership in class union....
eluni2 3805 Membership in class union....
elunii 3806 Membership in class union....
nfuni 3807 Bound-variable hypothesis ...
nfunid 3808 Deduction version of ~ nfu...
csbunig 3809 Distribute proper substitu...
unieq 3810 Equality theorem for class...
unieqi 3811 Inference of equality of t...
unieqd 3812 Deduction of equality of t...
eluniab 3813 Membership in union of a c...
elunirab 3814 Membership in union of a c...
unipr 3815 The union of a pair is the...
uniprg 3816 The union of a pair is the...
unisn 3817 A set equals the union of ...
unisng 3818 A set equals the union of ...
dfnfc2 3819 An alternative statement o...
uniun 3820 The class union of the uni...
uniin 3821 The class union of the int...
uniss 3822 Subclass relationship for ...
ssuni 3823 Subclass relationship for ...
unissi 3824 Subclass relationship for ...
unissd 3825 Subclass relationship for ...
uni0b 3826 The union of a set is empt...
uni0c 3827 The union of a set is empt...
uni0 3828 The union of the empty set...
elssuni 3829 An element of a class is a...
unissel 3830 Condition turning a subcla...
unissb 3831 Relationship involving mem...
uniss2 3832 A subclass condition on th...
unidif 3833 If the difference ` A \ B ...
ssunieq 3834 Relationship implying unio...
unimax 3835 Any member of a class is t...
dfint2 3838 Alternate definition of cl...
inteq 3839 Equality law for intersect...
inteqi 3840 Equality inference for cla...
inteqd 3841 Equality deduction for cla...
elint 3842 Membership in class inters...
elint2 3843 Membership in class inters...
elintg 3844 Membership in class inters...
elinti 3845 Membership in class inters...
nfint 3846 Bound-variable hypothesis ...
elintab 3847 Membership in the intersec...
elintrab 3848 Membership in the intersec...
elintrabg 3849 Membership in the intersec...
int0 3850 The intersection of the em...
intss1 3851 An element of a class incl...
ssint 3852 Subclass of a class inters...
ssintab 3853 Subclass of the intersecti...
ssintub 3854 Subclass of a least upper ...
ssmin 3855 Subclass of the minimum va...
intmin 3856 Any member of a class is t...
intss 3857 Intersection of subclasses...
intssuni 3858 The intersection of a none...
ssintrab 3859 Subclass of the intersecti...
unissint 3860 If the union of a class is...
intssuni2 3861 Subclass relationship for ...
intminss 3862 Under subset ordering, the...
intmin2 3863 Any set is the smallest of...
intmin3 3864 Under subset ordering, the...
intmin4 3865 Elimination of a conjunct ...
intab 3866 The intersection of a spec...
int0el 3867 The intersection of a clas...
intun 3868 The class intersection of ...
intpr 3869 The intersection of a pair...
intprg 3870 The intersection of a pair...
intsng 3871 Intersection of a singleto...
intsn 3872 The intersection of a sing...
uniintsn 3873 Two ways to express " ` A ...
uniintab 3874 The union and the intersec...
intunsn 3875 Theorem joining a singleto...
rint0 3876 Relative intersection of a...
elrint 3877 Membership in a restricted...
elrint2 3878 Membership in a restricted...
eliun 3883 Membership in indexed unio...
eliin 3884 Membership in indexed inte...
iuncom 3885 Commutation of indexed uni...
iuncom4 3886 Commutation of union with ...
iunconst 3887 Indexed union of a constan...
iinconst 3888 Indexed intersection of a ...
iuniin 3889 Law combining indexed unio...
iunss1 3890 Subclass theorem for index...
iinss1 3891 Subclass theorem for index...
iuneq1 3892 Equality theorem for index...
iineq1 3893 Equality theorem for restr...
ss2iun 3894 Subclass theorem for index...
iuneq2 3895 Equality theorem for index...
iineq2 3896 Equality theorem for index...
iuneq2i 3897 Equality inference for ind...
iineq2i 3898 Equality inference for ind...
iineq2d 3899 Equality deduction for ind...
iuneq2dv 3900 Equality deduction for ind...
iineq2dv 3901 Equality deduction for ind...
iuneq1d 3902 Equality theorem for index...
iuneq12d 3903 Equality deduction for ind...
iuneq2d 3904 Equality deduction for ind...
nfiun 3905 Bound-variable hypothesis ...
nfiin 3906 Bound-variable hypothesis ...
nfiu1 3907 Bound-variable hypothesis ...
nfii1 3908 Bound-variable hypothesis ...
dfiun2g 3909 Alternate definition of in...
dfiin2g 3910 Alternate definition of in...
dfiun2 3911 Alternate definition of in...
dfiin2 3912 Alternate definition of in...
cbviun 3913 Rule used to change the bo...
cbviin 3914 Change bound variables in ...
cbviunv 3915 Rule used to change the bo...
cbviinv 3916 Change bound variables in ...
iunss 3917 Subset theorem for an inde...
ssiun 3918 Subset implication for an ...
ssiun2 3919 Identity law for subset of...
ssiun2s 3920 Subset relationship for an...
iunss2 3921 A subclass condition on th...
iunab 3922 The indexed union of a cla...
iunrab 3923 The indexed union of a res...
iunxdif2 3924 Indexed union with a class...
ssiinf 3925 Subset theorem for an inde...
ssiin 3926 Subset theorem for an inde...
iinss 3927 Subset implication for an ...
iinss2 3928 An indexed intersection is...
uniiun 3929 Class union in terms of in...
intiin 3930 Class intersection in term...
iunid 3931 An indexed union of single...
iun0 3932 An indexed union of the em...
0iun 3933 An empty indexed union is ...
0iin 3934 An empty indexed intersect...
viin 3935 Indexed intersection with ...
iunn0 3936 There is a non-empty class...
iinab 3937 Indexed intersection of a ...
iinrab 3938 Indexed intersection of a ...
iinrab2 3939 Indexed intersection of a ...
iunin2 3940 Indexed union of intersect...
iunin1 3941 Indexed union of intersect...
iinun2 3942 Indexed intersection of un...
iundif2 3943 Indexed union of class dif...
2iunin 3944 Rearrange indexed unions o...
iindif2 3945 Indexed intersection of cl...
iinin2 3946 Indexed intersection of in...
iinin1 3947 Indexed intersection of in...
elriin 3948 Elementhood in a relative ...
riin0 3949 Relative intersection of a...
riinn0 3950 Relative intersection of a...
riinrab 3951 Relative intersection of a...
iinxsng 3952 A singleton index picks ou...
iinxprg 3953 Indexed intersection with ...
iunxsng 3954 A singleton index picks ou...
iunxsn 3955 A singleton index picks ou...
iunun 3956 Separate a union in an ind...
iunxun 3957 Separate a union in the in...
iunxiun 3958 Separate an indexed union ...
iinuni 3959 A relationship involving u...
iununi 3960 A relationship involving u...
sspwuni 3961 Subclass relationship for ...
pwssb 3962 Two ways to express a coll...
elpwuni 3963 Relationship for power cla...
iinpw 3964 The power class of an inte...
iunpwss 3965 Inclusion of an indexed un...
rintn0 3966 Relative intersection of a...
dfdisj2 3969 Alternate definition for d...
disjss2 3970 If each element of a colle...
disjeq2 3971 Equality theorem for disjo...
disjeq2dv 3972 Equality deduction for dis...
disjss1 3973 A subset of a disjoint col...
disjeq1 3974 Equality theorem for disjo...
disjeq1d 3975 Equality theorem for disjo...
disjeq12d 3976 Equality theorem for disjo...
cbvdisj 3977 Change bound variables in ...
cbvdisjv 3978 Change bound variables in ...
nfdisj 3979 Bound-variable hypothesis ...
nfdisj1 3980 Bound-variable hypothesis ...
disjor 3981 Two ways to say that a col...
disjmoOLD 3982 Two ways to say that a col...
disjors 3983 Two ways to say that a col...
disji2 3984 Property of a disjoint col...
disji 3985 Property of a disjoint col...
invdisj 3986 If there is a function ` C...
disjiun 3987 A disjoint collection yiel...
disjiunOLD 3988 A disjoint collection yiel...
sndisj 3989 Any collection of singleto...
0disj 3990 Any collection of empty se...
disjxsn 3991 A singleton collection is ...
disjx0 3992 An empty collection is dis...
disjprg 3993 A pair collection is disjo...
disjxiun 3994 An indexed union of a disj...
disjxun 3995 The union of two disjoint ...
disjss3 3996 Expand a disjoint collecti...
breq 3999 Equality theorem for binar...
breq1 4000 Equality theorem for a bin...
breq2 4001 Equality theorem for a bin...
breq12 4002 Equality theorem for a bin...
breqi 4003 Equality inference for bin...
breq1i 4004 Equality inference for a b...
breq2i 4005 Equality inference for a b...
breq12i 4006 Equality inference for a b...
breq1d 4007 Equality deduction for a b...
breqd 4008 Equality deduction for a b...
breq2d 4009 Equality deduction for a b...
breq12d 4010 Equality deduction for a b...
breq123d 4011 Equality deduction for a b...
breqan12d 4012 Equality deduction for a b...
breqan12rd 4013 Equality deduction for a b...
nbrne1 4014 Two classes are different ...
nbrne2 4015 Two classes are different ...
eqbrtri 4016 Substitution of equal clas...
eqbrtrd 4017 Substitution of equal clas...
eqbrtrri 4018 Substitution of equal clas...
eqbrtrrd 4019 Substitution of equal clas...
breqtri 4020 Substitution of equal clas...
breqtrd 4021 Substitution of equal clas...
breqtrri 4022 Substitution of equal clas...
breqtrrd 4023 Substitution of equal clas...
3brtr3i 4024 Substitution of equality i...
3brtr4i 4025 Substitution of equality i...
3brtr3d 4026 Substitution of equality i...
3brtr4d 4027 Substitution of equality i...
3brtr3g 4028 Substitution of equality i...
3brtr4g 4029 Substitution of equality i...
syl5eqbr 4030 B chained equality inferen...
syl5eqbrr 4031 B chained equality inferen...
syl5breq 4032 B chained equality inferen...
syl5breqr 4033 B chained equality inferen...
syl6eqbr 4034 A chained equality inferen...
syl6eqbrr 4035 A chained equality inferen...
syl6breq 4036 A chained equality inferen...
syl6breqr 4037 A chained equality inferen...
ssbrd 4038 Deduction from a subclass ...
ssbri 4039 Inference from a subclass ...
nfbrd 4040 Deduction version of bound...
nfbr 4041 Bound-variable hypothesis ...
brab1 4042 Relationship between a bin...
brun 4043 The union of two binary re...
brin 4044 The intersection of two re...
brdif 4045 The difference of two bina...
sbcbrg 4046 Move substitution in and o...
sbcbr12g 4047 Move substitution in and o...
sbcbr1g 4048 Move substitution in and o...
sbcbr2g 4049 Move substitution in and o...
opabss 4054 The collection of ordered ...
opabbid 4055 Equivalent wff's yield equ...
opabbidv 4056 Equivalent wff's yield equ...
opabbii 4057 Equivalent wff's yield equ...
nfopab 4058 Bound-variable hypothesis ...
nfopab1 4059 The first abstraction vari...
nfopab2 4060 The second abstraction var...
cbvopab 4061 Rule used to change bound ...
cbvopabv 4062 Rule used to change bound ...
cbvopab1 4063 Change first bound variabl...
cbvopab2 4064 Change second bound variab...
cbvopab1s 4065 Change first bound variabl...
cbvopab1v 4066 Rule used to change the fi...
cbvopab2v 4067 Rule used to change the se...
csbopabg 4068 Move substitution into a c...
unopab 4069 Union of two ordered pair ...
mpteq12f 4070 An equality theorem for th...
mpteq12dva 4071 An equality inference for ...
mpteq12dv 4072 An equality inference for ...
mpteq12 4073 An equality theorem for th...
mpteq1 4074 An equality theorem for th...
mpteq1d 4075 An equality theorem for th...
mpteq2ia 4076 An equality inference for ...
mpteq2i 4077 An equality inference for ...
mpteq12i 4078 An equality inference for ...
mpteq2da 4079 Slightly more general equa...
mpteq2dva 4080 Slightly more general equa...
mpteq2dv 4081 An equality inference for ...
nfmpt 4082 Bound-variable hypothesis ...
nfmpt1 4083 Bound-variable hypothesis ...
cbvmpt 4084 Rule to change the bound v...
cbvmptv 4085 Rule to change the bound v...
mptv 4086 Function with universal do...
dftr2 4089 An alternate way of defini...
dftr5 4090 An alternate way of defini...
dftr3 4091 An alternate way of defini...
dftr4 4092 An alternate way of defini...
treq 4093 Equality theorem for the t...
trel 4094 In a transitive class, the...
trel3 4095 In a transitive class, the...
trss 4096 An element of a transitive...
trin 4097 The intersection of transi...
tr0 4098 The empty set is transitiv...
trv 4099 The universe is transitive...
triun 4100 The indexed union of a cla...
truni 4101 The union of a class of tr...
trint 4102 The intersection of a clas...
trintss 4103 If ` A ` is transitive and...
trint0 4104 Any non-empty transitive c...
axrep1 4106 The version of the Axiom o...
axrep2 4107 Axiom of Replacement expre...
axrep3 4108 Axiom of Replacement sligh...
axrep4 4109 A more traditional version...
axrep5 4110 Axiom of Replacement (simi...
zfrepclf 4111 An inference rule based on...
zfrep3cl 4112 An inference rule based on...
zfrep4 4113 A version of Replacement u...
axsep 4114 Separation Scheme, which i...
axsep2 4116 A less restrictive version...
zfauscl 4117 Separation Scheme (Aussond...
bm1.3ii 4118 Convert implication to equ...
ax9vsep 4119 Derive a weakened version ...
zfnuleu 4120 Show the uniqueness of the...
axnulALT 4121 Prove ~ axnul directly fro...
axnul 4122 The Null Set Axiom of ZF s...
0ex 4124 The Null Set Axiom of ZF s...
nalset 4125 No set contains all sets. ...
vprc 4126 The universal class is not...
nvel 4127 The universal class doesn'...
vnex 4128 The universal class does n...
inex1 4129 Separation Scheme (Aussond...
inex2 4130 Separation Scheme (Aussond...
inex1g 4131 Closed-form, generalized S...
ssex 4132 The subset of a set is als...
ssexi 4133 The subset of a set is als...
ssexg 4134 The subset of a set is als...
ssexd 4135 A subclass of a set is a s...
difexg 4136 Existence of a difference....
zfausab 4137 Separation Scheme (Aussond...
rabexg 4138 Separation Scheme in terms...
rabex 4139 Separation Scheme in terms...
elssabg 4140 Membership in a class abst...
elpw2g 4141 Membership in a power clas...
elpw2 4142 Membership in a power clas...
intex 4143 The intersection of a non-...
intnex 4144 If a class intersection is...
intexab 4145 The intersection of a non-...
intexrab 4146 The intersection of a non-...
iinexg 4147 The existence of an indexe...
intabs 4148 Absorption of a redundant ...
inuni 4149 The intersection of a unio...
class2set 4150 Construct, from any class ...
class2seteq 4151 Equality theorem based on ...
0elpw 4152 Every power class contains...
0nep0 4153 The empty set and its powe...
0inp0 4154 Something cannot be equal ...
unidif0 4155 The removal of the empty s...
iin0 4156 An indexed intersection of...
notzfaus 4157 In the Separation Scheme ~...
intv 4158 The intersection of the un...
axpweq 4159 Two equivalent ways to exp...
zfpow 4161 Axiom of Power Sets expres...
axpow2 4162 A variant of the Axiom of ...
axpow3 4163 A variant of the Axiom of ...
el 4164 Every set is an element of...
pwex 4165 Power set axiom expressed ...
pwexg 4166 Power set axiom expressed ...
abssexg 4167 Existence of a class of su...
snexALT 4168 A singleton is a set. The...
p0ex 4169 The power set of the empty...
p0exALT 4170 The power set of the empty...
pp0ex 4171 The power set of the power...
ord3ex 4172 The ordinal number 3 is a ...
dtru 4173 At least two sets exist (o...
ax16b 4174 This theorem shows that ax...
eunex 4175 Existential uniqueness imp...
nfnid 4176 A set variable is not free...
nfcvb 4177 The "distinctor" expressio...
pwuni 4178 A class is a subclass of t...
dtruALT 4179 A version of ~ dtru ("two ...
dtrucor 4180 Corollary of ~ dtru . Thi...
dtrucor2 4181 The theorem form of the de...
dvdemo1 4182 Demonstration of a theorem...
dvdemo2 4183 Demonstration of a theorem...
zfpair 4184 The Axiom of Pairing of Ze...
axpr 4185 Unabbreviated version of t...
zfpair2 4187 Derive the abbreviated ver...
snex 4188 A singleton is a set. The...
prex 4189 The Axiom of Pairing using...
elALT 4190 Every set is an element of...
dtruALT2 4191 An alternative proof of ~ ...
snelpwi 4192 A singleton of a set belon...
snelpw 4193 A singleton of a set belon...
rext 4194 A theorem similar to exten...
sspwb 4195 Classes are subclasses if ...
unipw 4196 A class equals the union o...
pwel 4197 Membership of a power clas...
pwtr 4198 A class is transitive iff ...
ssextss 4199 An extensionality-like pri...
ssext 4200 An extensionality-like pri...
nssss 4201 Negation of subclass relat...
pweqb 4202 Classes are equal if and o...
intid 4203 The intersection of all se...
moabex 4204 "At most one" existence im...
rmorabex 4205 Restricted "at most one" e...
euabex 4206 The abstraction of a wff w...
nnullss 4207 A non-empty class (even if...
exss 4208 Restricted existence in a ...
opex 4209 An ordered pair of classes...
otex 4210 An ordered triple of class...
elop 4211 An ordered pair has two el...
opi1 4212 One of the two elements in...
opi2 4213 One of the two elements of...
opnz 4214 An ordered pair is nonempt...
opnzi 4215 An ordered pair is nonempt...
opth1 4216 Equality of the first memb...
opth 4217 The ordered pair theorem. ...
opthg 4218 Ordered pair theorem. ` C ...
opthg2 4219 Ordered pair theorem. (Co...
opth2 4220 Ordered pair theorem. (Co...
otth2 4221 Ordered triple theorem, wi...
otth 4222 Ordered triple theorem. (...
eqvinop 4223 A variable introduction la...
copsexg 4224 Substitution of class ` A ...
copsex2t 4225 Closed theorem form of ~ c...
copsex2g 4226 Implicit substitution infe...
copsex4g 4227 An implicit substitution i...
0nelop 4228 A property of ordered pair...
opeqex 4229 Equivalence of existence i...
oteqex2 4230 Equivalence of existence i...
oteqex 4231 Equivalence of existence i...
opcom 4232 An ordered pair commutes i...
moop2 4233 "At most one" property of ...
opeqsn 4234 Equivalence for an ordered...
opeqpr 4235 Equivalence for an ordered...
mosubopt 4236 "At most one" remains true...
mosubop 4237 "At most one" remains true...
euop2 4238 Transfer existential uniqu...
euotd 4239 Prove existential uniquene...
opthwiener 4240 Justification theorem for ...
uniop 4241 The union of an ordered pa...
uniopel 4242 Ordered pair membership is...
opabid 4243 The law of concretion. Sp...
elopab 4244 Membership in a class abst...
opelopabsbOLD 4245 The law of concretion in t...
brabsbOLD 4246 The law of concretion in t...
opelopabsb 4247 The law of concretion in t...
brabsb 4248 The law of concretion in t...
opelopabt 4249 Closed theorem form of ~ o...
opelopabga 4250 The law of concretion. Th...
brabga 4251 The law of concretion for ...
opelopab2a 4252 Ordered pair membership in...
opelopaba 4253 The law of concretion. Th...
braba 4254 The law of concretion for ...
opelopabg 4255 The law of concretion. Th...
brabg 4256 The law of concretion for ...
opelopab2 4257 Ordered pair membership in...
opelopab 4258 The law of concretion. Th...
brab 4259 The law of concretion for ...
opelopabaf 4260 The law of concretion. Th...
opelopabf 4261 The law of concretion. Th...
ssopab2 4262 Equivalence of ordered pai...
ssopab2b 4263 Equivalence of ordered pai...
ssopab2i 4264 Inference of ordered pair ...
ssopab2dv 4265 Inference of ordered pair ...
eqopab2b 4266 Equivalence of ordered pai...
opabn0 4267 Non-empty ordered pair cla...
iunopab 4268 Move indexed union inside ...
pwin 4269 The power class of the int...
pwunss 4270 The power class of the uni...
pwssun 4271 The power class of the uni...
pwundif 4272 Break up the power class o...
pwundifOLD 4273 Break up the power class o...
pwun 4274 The power class of the uni...
epelg 4278 The epsilon relation and m...
epelc 4279 The epsilon relationship a...
epel 4280 The epsilon relation and t...
dfid3 4282 A stronger version of ~ df...
dfid2 4283 Alternate definition of th...
poss 4288 Subset theorem for the par...
poeq1 4289 Equality theorem for parti...
poeq2 4290 Equality theorem for parti...
nfpo 4291 Bound-variable hypothesis ...
nfso 4292 Bound-variable hypothesis ...
pocl 4293 Properties of partial orde...
ispod 4294 Sufficient conditions for ...
swopolem 4295 Perform the substitutions ...
swopo 4296 A strict weak order is a p...
poirr 4297 A partial order relation i...
potr 4298 A partial order relation i...
po2nr 4299 A partial order relation h...
po3nr 4300 A partial order relation h...
po0 4301 Any relation is a partial ...
pofun 4302 A function preserves a par...
sopo 4303 A strict linear order is a...
soss 4304 Subset theorem for the str...
soeq1 4305 Equality theorem for the s...
soeq2 4306 Equality theorem for the s...
sonr 4307 A strict order relation is...
sotr 4308 A strict order relation is...
solin 4309 A strict order relation is...
so2nr 4310 A strict order relation ha...
so3nr 4311 A strict order relation ha...
sotric 4312 A strict order relation sa...
sotrieq 4313 Trichotomy law for strict ...
sotrieq2 4314 Trichotomy law for strict ...
sotr2 4315 A transitivity relation. ...
issod 4316 A irreflexive, transitive,...
issoi 4317 A irreflexive, transitive,...
isso2i 4318 Deduce strict ordering fro...
so0 4319 Any relation is a strict o...
somo 4320 A totally ordered set has ...
fri 4327 Property of well-founded r...
seex 4328 The ` R ` -preimage of an ...
exse 4329 Any relation on a set is s...
dffr2 4330 Alternate definition of we...
frc 4331 Property of well-founded r...
frss 4332 Subset theorem for the wel...
sess1 4333 Subset theorem for the set...
sess2 4334 Subset theorem for the set...
freq1 4335 Equality theorem for the w...
freq2 4336 Equality theorem for the w...
seeq1 4337 Equality theorem for the s...
seeq2 4338 Equality theorem for the s...
nffr 4339 Bound-variable hypothesis ...
nfse 4340 Bound-variable hypothesis ...
nfwe 4341 Bound-variable hypothesis ...
frirr 4342 A well-founded relation is...
fr2nr 4343 A well-founded relation ha...
fr0 4344 Any relation is well-found...
frminex 4345 If an element of a well-fo...
efrirr 4346 Irreflexivity of the epsil...
efrn2lp 4347 A set founded by epsilon c...
epse 4348 The epsilon relation is se...
tz7.2 4349 Similar to Theorem 7.2 of ...
dfepfr 4350 An alternate way of saying...
epfrc 4351 A subset of an epsilon-fou...
wess 4352 Subset theorem for the wel...
weeq1 4353 Equality theorem for the w...
weeq2 4354 Equality theorem for the w...
wefr 4355 A well-ordering is well-fo...
weso 4356 A well-ordering is a stric...
wecmpep 4357 The elements of an epsilon...
wetrep 4358 An epsilon well-ordering i...
wefrc 4359 A non-empty (possibly prop...
we0 4360 Any relation is a well-ord...
wereu 4361 A subset of a well-ordered...
wereu2 4362 All nonempty (possibly pro...
ordeq 4371 Equality theorem for the o...
elong 4372 An ordinal number is an or...
elon 4373 An ordinal number is an or...
eloni 4374 An ordinal number has the ...
elon2 4375 An ordinal number is an or...
limeq 4376 Equality theorem for the l...
ordwe 4377 Epsilon well orders every ...
ordtr 4378 An ordinal class is transi...
ordfr 4379 Epsilon is well-founded on...
ordelss 4380 An element of an ordinal c...
trssord 4381 A transitive subclass of a...
ordirr 4382 Epsilon irreflexivity of o...
nordeq 4383 A member of an ordinal cla...
ordn2lp 4384 An ordinal class cannot an...
tz7.5 4385 A subclass (possibly prope...
ordelord 4386 An element of an ordinal c...
tron 4387 The class of all ordinal n...
ordelon 4388 An element of an ordinal c...
onelon 4389 An element of an ordinal n...
tz7.7 4390 Proposition 7.7 of [Takeut...
ordelssne 4391 Corollary 7.8 of [TakeutiZ...
ordelpss 4392 Corollary 7.8 of [TakeutiZ...
ordsseleq 4393 For ordinal classes, subcl...
ordin 4394 The intersection of two or...
onin 4395 The intersection of two or...
ordtri3or 4396 A trichotomy law for ordin...
ordtri1 4397 A trichotomy law for ordin...
ontri1 4398 A trichotomy law for ordin...
ordtri2 4399 A trichotomy law for ordin...
ordtri3 4400 A trichotomy law for ordin...
ordtri4 4401 A trichotomy law for ordin...
orddisj 4402 An ordinal class and its s...
onfr 4403 The ordinal class is well-...
onelpss 4404 Relationship between membe...
onsseleq 4405 Relationship between subse...
onelss 4406 An element of an ordinal n...
ordtr1 4407 Transitive law for ordinal...
ordtr2 4408 Transitive law for ordinal...
ordtr3 4409 Transitive law for ordinal...
ontr1 4410 Transitive law for ordinal...
ontr2 4411 Transitive law for ordinal...
ordunidif 4412 The union of an ordinal st...
ordintdif 4413 If ` B ` is smaller than `...
onintss 4414 If a property is true for ...
oneqmini 4415 A way to show that an ordi...
ord0 4416 The empty set is an ordina...
0elon 4417 The empty set is an ordina...
ord0eln0 4418 A non-empty ordinal contai...
on0eln0 4419 An ordinal number contains...
dflim2 4420 An alternate definition of...
inton 4421 The intersection of the cl...
nlim0 4422 The empty set is not a lim...
limord 4423 A limit ordinal is ordinal...
limuni 4424 A limit ordinal is its own...
limuni2 4425 The union of a limit ordin...
0ellim 4426 A limit ordinal contains t...
limelon 4427 A limit ordinal class that...
onn0 4428 The class of all ordinal n...
suceq 4429 Equality of successors. (...
elsuci 4430 Membership in a successor....
elsucg 4431 Membership in a successor....
elsuc2g 4432 Variant of membership in a...
elsuc 4433 Membership in a successor....
elsuc2 4434 Membership in a successor....
nfsuc 4435 Bound-variable hypothesis ...
elelsuc 4436 Membership in a successor....
sucel 4437 Membership of a successor ...
suc0 4438 The successor of the empty...
sucprc 4439 A proper class is its own ...
unisuc 4440 A transitive class is equa...
sssucid 4441 A class is included in its...
sucidg 4442 Part of Proposition 7.23 o...
sucid 4443 A set belongs to its succe...
nsuceq0 4444 No successor is empty. (C...
eqelsuc 4445 A set belongs to the succe...
iunsuc 4446 Inductive definition for t...
suctr 4447 The successor of a transti...
trsuc 4448 A set whose successor belo...
trsuc2OLD 4449 Obsolete proof of ~ suctr ...
trsucss 4450 A member of the successor ...
ordsssuc 4451 A subset of an ordinal bel...
onsssuc 4452 A subset of an ordinal num...
ordsssuc2 4453 An ordinal subset of an or...
onmindif 4454 When its successor is subt...
ordnbtwn 4455 There is no set between an...
onnbtwn 4456 There is no set between an...
sucssel 4457 A set whose successor is a...
orddif 4458 Ordinal derived from its s...
orduniss 4459 An ordinal class includes ...
ordtri2or 4460 A trichotomy law for ordin...
ordtri2or2 4461 A trichotomy law for ordin...
ordtri2or3 4462 A consequence of total ord...
ordelinel 4463 The intersection of two or...
ordssun 4464 Property of a subclass of ...
ordequn 4465 The maximum (i.e. union) o...
ordun 4466 The maximum (i.e. union) o...
ordunisssuc 4467 A subclass relationship fo...
suc11 4468 The successor operation be...
onordi 4469 An ordinal number is an or...
ontrci 4470 An ordinal number is a tra...
onirri 4471 An ordinal number is not a...
oneli 4472 A member of an ordinal num...
onelssi 4473 A member of an ordinal num...
onssneli 4474 An ordering law for ordina...
onssnel2i 4475 An ordering law for ordina...
onelini 4476 An element of an ordinal n...
oneluni 4477 An ordinal number equals i...
onunisuci 4478 An ordinal number is equal...
onsseli 4479 Subset is equivalent to me...
onun2i 4480 The union of two ordinal n...
unizlim 4481 An ordinal equal to its ow...
on0eqel 4482 An ordinal number either e...
snsn0non 4483 The singleton of the singl...
zfun 4485 Axiom of Union expressed w...
axun2 4486 A variant of the Axiom of ...
uniex2 4487 The Axiom of Union using t...
uniex 4488 The Axiom of Union in clas...
uniexg 4489 The ZF Axiom of Union in c...
unex 4490 The union of two sets is a...
tpex 4491 A triple of classes exists...
unexb 4492 Existence of union is equi...
unexg 4493 A union of two sets is a s...
unisn2 4494 A version of ~ unisn witho...
unisn3 4495 Union of a singleton in th...
snnex 4496 The class of all singleton...
difex2 4497 If the subtrahend of a cla...
opeluu 4498 Each member of an ordered ...
uniuni 4499 Expression for double unio...
eusv1 4500 Two ways to express single...
eusvnf 4501 Even if ` x ` is free in `...
eusvnfb 4502 Two ways to say that ` A (...
eusv2i 4503 Two ways to express single...
eusv2nf 4504 Two ways to express single...
eusv2 4505 Two ways to express single...
reusv1 4506 Two ways to express single...
reusv2lem1 4507 Lemma for ~ reusv2 . (Con...
reusv2lem2 4508 Lemma for ~ reusv2 . (Con...
reusv2lem3 4509 Lemma for ~ reusv2 . (Con...
reusv2lem4 4510 Lemma for ~ reusv2 . (Con...
reusv2lem5 4511 Lemma for ~ reusv2 . (Con...
reusv2 4512 Two ways to express single...
reusv3i 4513 Two ways of expressing exi...
reusv3 4514 Two ways to express single...
eusv4 4515 Two ways to express single...
reusv5OLD 4516 Two ways to express single...
reusv6OLD 4517 Two ways to express single...
reusv7OLD 4518 Two ways to express single...
alxfr 4519 Transfer universal quantif...
ralxfrd 4520 Transfer universal quantif...
rexxfrd 4521 Transfer universal quantif...
ralxfr2d 4522 Transfer universal quantif...
rexxfr2d 4523 Transfer universal quantif...
ralxfr 4524 Transfer universal quantif...
ralxfrALT 4525 Transfer universal quantif...
rexxfr 4526 Transfer existence from a ...
rabxfrd 4527 Class builder membership a...
rabxfr 4528 Class builder membership a...
reuxfr2d 4529 Transfer existential uniqu...
reuxfr2 4530 Transfer existential uniqu...
reuxfrd 4531 Transfer existential uniqu...
reuxfr 4532 Transfer existential uniqu...
reuhypd 4533 A theorem useful for elimi...
reuhyp 4534 A theorem useful for elimi...
uniexb 4535 The Axiom of Union and its...
pwexb 4536 The Axiom of Power Sets an...
univ 4537 The union of the universe ...
eldifpw 4538 Membership in a power clas...
elpwun 4539 Membership in the power cl...
elpwunsn 4540 Membership in an extension...
op1stb 4541 Extract the first member o...
iunpw 4542 An indexed union of a powe...
fr3nr 4543 A well-founded relation ha...
epne3 4544 A set well-founded by epsi...
dfwe2 4545 Alternate definition of we...
ordon 4546 The class of all ordinal n...
epweon 4547 The epsilon relation well-...
onprc 4548 No set contains all ordina...
ssorduni 4549 The union of a class of or...
ssonuni 4550 The union of a set of ordi...
ssonunii 4551 The union of a set of ordi...
ordeleqon 4552 A way to express the ordin...
ordsson 4553 Any ordinal class is a sub...
onss 4554 An ordinal number is a sub...
ssonprc 4555 Two ways of saying a class...
onuni 4556 The union of an ordinal nu...
orduni 4557 The union of an ordinal cl...
onint 4558 The intersection (infimum)...
onint0 4559 The intersection of a clas...
onssmin 4560 A non-empty class of ordin...
onminesb 4561 If a property is true for ...
onminsb 4562 If a property is true for ...
oninton 4563 The intersection of a non-...
onintrab 4564 The intersection of a clas...
onintrab2 4565 An existence condition equ...
onnmin 4566 No member of a set of ordi...
onnminsb 4567 An ordinal number smaller ...
oneqmin 4568 A way to show that an ordi...
bm2.5ii 4569 Problem 2.5(ii) of [BellMa...
onminex 4570 If a wff is true for an or...
sucon 4571 The class of all ordinal n...
sucexb 4572 A successor exists iff its...
sucexg 4573 The successor of a set is ...
sucex 4574 The successor of a set is ...
onmindif2 4575 The minimum of a class of ...
suceloni 4576 The successor of an ordina...
ordsuc 4577 The successor of an ordina...
ordpwsuc 4578 The collection of ordinals...
onpwsuc 4579 The collection of ordinal ...
sucelon 4580 The successor of an ordina...
ordsucss 4581 The successor of an elemen...
onpsssuc 4582 An ordinal number is a pro...
ordelsuc 4583 A set belongs to an ordina...
onsucmin 4584 The successor of an ordina...
ordsucelsuc 4585 Membership is inherited by...
ordsucsssuc 4586 The subclass relationship ...
ordsucuniel 4587 Given an element ` A ` of ...
ordsucun 4588 The successor of the maxim...
ordunpr 4589 The maximum of two ordinal...
ordunel 4590 The maximum of two ordinal...
onsucuni 4591 A class of ordinal numbers...
ordsucuni 4592 An ordinal class is a subc...
orduniorsuc 4593 An ordinal class is either...
unon 4594 The class of all ordinal n...
ordunisuc 4595 An ordinal class is equal ...
orduniss2 4596 The union of the ordinal s...
onsucuni2 4597 A successor ordinal is the...
0elsuc 4598 The successor of an ordina...
limon 4599 The class of ordinal numbe...
onssi 4600 An ordinal number is a sub...
onsuci 4601 The successor of an ordina...
onuniorsuci 4602 An ordinal number is eithe...
onuninsuci 4603 A limit ordinal is not a s...
onsucssi 4604 A set belongs to an ordina...
nlimsucg 4605 A successor is not a limit...
orduninsuc 4606 An ordinal equal to its un...
ordunisuc2 4607 An ordinal equal to its un...
ordzsl 4608 An ordinal is zero, a succ...
onzsl 4609 An ordinal number is zero,...
dflim3 4610 An alternate definition of...
dflim4 4611 An alternate definition of...
limsuc 4612 The successor of a member ...
limsssuc 4613 A class includes a limit o...
nlimon 4614 Two ways to express the cl...
limuni3 4615 The union of a nonempty cl...
tfi 4616 The Principle of Transfini...
tfis 4617 Transfinite Induction Sche...
tfis2f 4618 Transfinite Induction Sche...
tfis2 4619 Transfinite Induction Sche...
tfis3 4620 Transfinite Induction Sche...
tfisi 4621 A transfinite induction sc...
tfinds 4622 Principle of Transfinite I...
tfindsg 4623 Transfinite Induction (inf...
tfindsg2 4624 Transfinite Induction (inf...
tfindes 4625 Transfinite Induction with...
tfinds2 4626 Transfinite Induction (inf...
tfinds3 4627 Principle of Transfinite I...
dfom2 4630 An alternate definition of...
elom 4631 Membership in omega. The ...
omsson 4632 Omega is a subset of ` On ...
limomss 4633 The class of natural numbe...
nnon 4634 A natural number is an ord...
nnoni 4635 A natural number is an ord...
nnord 4636 A natural number is ordina...
ordom 4637 Omega is ordinal. Theorem...
elnn 4638 A member of a natural numb...
omon 4639 The class of natural numbe...
omelon2 4640 Omega is an ordinal number...
nnlim 4641 A natural number is not a ...
omssnlim 4642 The class of natural numbe...
limom 4643 Omega is a limit ordinal. ...
peano2b 4644 A class belongs to omega i...
nnsuc 4645 A nonzero natural number i...
ssnlim 4646 An ordinal subclass of non...
peano1 4647 Zero is a natural number. ...
peano2 4648 The successor of any natur...
peano3 4649 The successor of any natur...
peano4 4650 Two natural numbers are eq...
peano5 4651 The induction postulate: a...
nn0suc 4652 A natural number is either...
find 4653 The Principle of Finite In...
finds 4654 Principle of Finite Induct...
findsg 4655 Principle of Finite Induct...
finds2 4656 Principle of Finite Induct...
finds1 4657 Principle of Finite Induct...
findes 4658 Finite induction with expl...
xpeq1 4691 Equality theorem for cross...
xpeq2 4692 Equality theorem for cross...
elxpi 4693 Membership in a cross prod...
elxp 4694 Membership in a cross prod...
elxp2 4695 Membership in a cross prod...
xpeq12 4696 Equality theorem for cross...
xpeq1i 4697 Equality inference for cro...
xpeq2i 4698 Equality inference for cro...
xpeq12i 4699 Equality inference for cro...
xpeq1d 4700 Equality deduction for cro...
xpeq2d 4701 Equality deduction for cro...
xpeq12d 4702 Equality deduction for cro...
nfxp 4703 Bound-variable hypothesis ...
csbxpg 4704 Distribute proper substitu...
0nelxp 4705 The empty set is not a mem...
0nelelxp 4706 A member of a cross produc...
opelxp 4707 Ordered pair membership in...
brxp 4708 Binary relation on a cross...
opelxpi 4709 Ordered pair membership in...
opelxp1 4710 The first member of an ord...
opelxp2 4711 The second member of an or...
otelxp1 4712 The first member of an ord...
rabxp 4713 Membership in a class buil...
brrelex12 4714 A true binary relation on ...
brrelex 4715 A true binary relation on ...
brrelex2 4716 A true binary relation on ...
brrelexi 4717 The first argument of a bi...
brrelex2i 4718 The second argument of a b...
nprrel 4719 No proper class is related...
fconstmpt 4720 Representation of a consta...
vtoclr 4721 Variable to class conversi...
opelvvg 4722 Ordered pair membership in...
opelvv 4723 Ordered pair membership in...
opthprc 4724 Justification theorem for ...
brel 4725 Two things in a binary rel...
brab2a 4726 Ordered pair membership in...
elxp3 4727 Membership in a cross prod...
opeliunxp 4728 Membership in a union of c...
xpundi 4729 Distributive law for cross...
xpundir 4730 Distributive law for cross...
xpiundi 4731 Distributive law for cross...
xpiundir 4732 Distributive law for cross...
resiundiOLD 4733 Obsolete proof of ~ resiun...
iunxpconst 4734 Membership in a union of c...
xpun 4735 The cross product of two u...
elvv 4736 Membership in universal cl...
elvvv 4737 Membership in universal cl...
elvvuni 4738 An ordered pair contains i...
brinxp2 4739 Intersection of binary rel...
brinxp 4740 Intersection of binary rel...
poinxp 4741 Intersection of partial or...
soinxp 4742 Intersection of total orde...
frinxp 4743 Intersection of well-found...
seinxp 4744 Intersection of set-like r...
weinxp 4745 Intersection of well-order...
posn 4746 Partial ordering of a sing...
sosn 4747 Strict ordering on a singl...
frsn 4748 Founded relation on a sing...
wesn 4749 Well-ordering of a singlet...
opabssxp 4750 An abstraction relation is...
brab2ga 4751 The law of concretion for ...
optocl 4752 Implicit substitution of c...
2optocl 4753 Implicit substitution of c...
3optocl 4754 Implicit substitution of c...
opbrop 4755 Ordered pair membership in...
xp0r 4756 The cross product with the...
onxpdisj 4757 Ordinal numbers and ordere...
onnev 4758 The class of ordinal numbe...
releq 4759 Equality theorem for the r...
releqi 4760 Equality inference for the...
releqd 4761 Equality deduction for the...
nfrel 4762 Bound-variable hypothesis ...
relss 4763 Subclass theorem for relat...
ssrel 4764 A subclass relationship de...
eqrel 4765 Extensionality principle f...
relssi 4766 Inference from subclass pr...
relssdv 4767 Deduction from subclass pr...
eqrelriv 4768 Inference from extensional...
eqrelriiv 4769 Inference from extensional...
eqbrriv 4770 Inference from extensional...
eqrelrdv 4771 Deduce equality of relatio...
eqbrrdv 4772 Deduction from extensional...
eqbrrdiv 4773 Deduction from extensional...
eqrelrdv2 4774 A version of ~ eqrelrdv . ...
ssrelrel 4775 A subclass relationship de...
eqrelrel 4776 Extensionality principle f...
elrel 4777 A member of a relation is ...
relsn 4778 A singleton is a relation ...
relsnop 4779 A singleton of an ordered ...
xpss12 4780 Subset theorem for cross p...
xpss 4781 A cross product is include...
relxp 4782 A cross product is a relat...
xpss1 4783 Subset relation for cross ...
xpss2 4784 Subset relation for cross ...
xpsspw 4785 A cross product is include...
xpsspwOLD 4786 A cross product is include...
unixpss 4787 The double class union of ...
xpexg 4788 The cross product of two s...
xpex 4789 The cross product of two s...
relun 4790 The union of two relations...
relin1 4791 The intersection with a re...
relin2 4792 The intersection with a re...
reldif 4793 A difference cutting down ...
reliun 4794 An indexed union is a rela...
reliin 4795 An indexed intersection is...
reluni 4796 The union of a class is a ...
relint 4797 The intersection of a clas...
rel0 4798 The empty set is a relatio...
relopabi 4799 A class of ordered pairs i...
relopab 4800 A class of ordered pairs i...
reli 4801 The identity relation is a...
rele 4802 The membership relation is...
opabid2 4803 A relation expressed as an...
inopab 4804 Intersection of two ordere...
difopab 4805 The difference of two orde...
inxp 4806 The intersection of two cr...
xpindi 4807 Distributive law for cross...
xpindir 4808 Distributive law for cross...
xpiindi 4809 Distributive law for cross...
xpriindi 4810 Distributive law for cross...
eliunxp 4811 Membership in a union of c...
opeliunxp2 4812 Membership in a union of c...
raliunxp 4813 Write a double restricted ...
rexiunxp 4814 Write a double restricted ...
ralxp 4815 Universal quantification r...
rexxp 4816 Existential quantification...
djussxp 4817 Disjoint union is a subset...
ralxpf 4818 Version of ~ ralxp with bo...
rexxpf 4819 Version of ~ rexxp with bo...
iunxpf 4820 Indexed union on a cross p...
opabbi2dv 4821 Deduce equality of a relat...
relop 4822 A necessary and sufficient...
ideqg 4823 For sets, the identity rel...
ideq 4824 For sets, the identity rel...
ididg 4825 A set is identical to itse...
issetid 4826 Two ways of expressing set...
coss1 4827 Subclass theorem for compo...
coss2 4828 Subclass theorem for compo...
coeq1 4829 Equality theorem for compo...
coeq2 4830 Equality theorem for compo...
coeq1i 4831 Equality inference for com...
coeq2i 4832 Equality inference for com...
coeq1d 4833 Equality deduction for com...
coeq2d 4834 Equality deduction for com...
coeq12i 4835 Equality inference for com...
coeq12d 4836 Equality deduction for com...
nfco 4837 Bound-variable hypothesis ...
brcog 4838 Ordered pair membership in...
opelco2g 4839 Ordered pair membership in...
brco 4840 Binary relation on a compo...
opelco 4841 Ordered pair membership in...
cnvss 4842 Subset theorem for convers...
cnveq 4843 Equality theorem for conve...
cnveqi 4844 Equality inference for con...
cnveqd 4845 Equality deduction for con...
elcnv 4846 Membership in a converse. ...
elcnv2 4847 Membership in a converse. ...
nfcnv 4848 Bound-variable hypothesis ...
opelcnvg 4849 Ordered-pair membership in...
brcnvg 4850 The converse of a binary r...
opelcnv 4851 Ordered-pair membership in...
brcnv 4852 The converse of a binary r...
cnvco 4853 Distributive law of conver...
cnvuni 4854 The converse of a class un...
dfdm3 4855 Alternate definition of do...
dfrn2 4856 Alternate definition of ra...
dfrn3 4857 Alternate definition of ra...
elrn2g 4858 Membership in a range. (C...
elrng 4859 Membership in a range. (C...
dfdm4 4860 Alternate definition of do...
dfdmf 4861 Definition of domain, usin...
eldmg 4862 Domain membership. Theore...
eldm2g 4863 Domain membership. Theore...
eldm 4864 Membership in a domain. T...
eldm2 4865 Membership in a domain. T...
dmss 4866 Subset theorem for domain....
dmeq 4867 Equality theorem for domai...
dmeqi 4868 Equality inference for dom...
dmeqd 4869 Equality deduction for dom...
opeldm 4870 Membership of first of an ...
breldm 4871 Membership of first of a b...
breldmg 4872 Membership of first of a b...
dmun 4873 The domain of a union is t...
dmin 4874 The domain of an intersect...
dmiun 4875 The domain of an indexed u...
dmuni 4876 The domain of a union. Pa...
dmopab 4877 The domain of a class of o...
dmopabss 4878 Upper bound for the domain...
dmopab3 4879 The domain of a restricted...
dm0 4880 The domain of the empty se...
dmi 4881 The domain of the identity...
dmv 4882 The domain of the universe...
dm0rn0 4883 An empty domain implies an...
reldm0 4884 A relation is empty iff it...
dmxp 4885 The domain of a cross prod...
dmxpid 4886 The domain of a square cro...
dmxpin 4887 The domain of the intersec...
xpid11 4888 The cross product of a cla...
dmcnvcnv 4889 The domain of the double c...
rncnvcnv 4890 The range of the double co...
elreldm 4891 The first member of an ord...
rneq 4892 Equality theorem for range...
rneqi 4893 Equality inference for ran...
rneqd 4894 Equality deduction for ran...
rnss 4895 Subset theorem for range. ...
brelrng 4896 The second argument of a b...
brelrn 4897 The second argument of a b...
opelrn 4898 Membership of second membe...
releldm 4899 The first argument of a bi...
relelrn 4900 The second argument of a b...
releldmb 4901 Membership in a domain. (...
relelrnb 4902 Membership in a range. (C...
releldmi 4903 The first argument of a bi...
relelrni 4904 The second argument of a b...
dfrnf 4905 Definition of range, using...
elrn2 4906 Membership in a range. (C...
elrn 4907 Membership in a range. (C...
nfdm 4908 Bound-variable hypothesis ...
nfrn 4909 Bound-variable hypothesis ...
dmiin 4910 Domain of an intersection....
csbrng 4911 Distribute proper substitu...
rnopab 4912 The range of a class of or...
rnmpt 4913 The range of a function in...
elrnmpt 4914 The range of a function in...
elrnmpt1s 4915 Elementhood in an image se...
elrnmpt1 4916 Elementhood in an image se...
elrnmptg 4917 Membership in the range of...
elrnmpti 4918 Membership in the range of...
dfiun3g 4919 Alternate definition of in...
dfiin3g 4920 Alternate definition of in...
dfiun3 4921 Alternate definition of in...
dfiin3 4922 Alternate definition of in...
riinint 4923 Express a relative indexed...
rn0 4924 The range of the empty set...
relrn0 4925 A relation is empty iff it...
dmrnssfld 4926 The domain and range of a ...
dmexg 4927 The domain of a set is a s...
rnexg 4928 The range of a set is a se...
dmex 4929 The domain of a set is a s...
rnex 4930 The range of a set is a se...
iprc 4931 The identity function is a...
dmcoss 4932 Domain of a composition. ...
rncoss 4933 Range of a composition. (...
dmcosseq 4934 Domain of a composition. ...
dmcoeq 4935 Domain of a composition. ...
rncoeq 4936 Range of a composition. (...
reseq1 4937 Equality theorem for restr...
reseq2 4938 Equality theorem for restr...
reseq1i 4939 Equality inference for res...
reseq2i 4940 Equality inference for res...
reseq12i 4941 Equality inference for res...
reseq1d 4942 Equality deduction for res...
reseq2d 4943 Equality deduction for res...
reseq12d 4944 Equality deduction for res...
nfres 4945 Bound-variable hypothesis ...
csbresg 4946 Distribute proper substitu...
res0 4947 A restriction to the empty...
opelres 4948 Ordered pair membership in...
brres 4949 Binary relation on a restr...
opelresg 4950 Ordered pair membership in...
brresg 4951 Binary relation on a restr...
opres 4952 Ordered pair membership in...
resieq 4953 A restricted identity rela...
opelresiOLD 4954 ` <. A , A >. ` belongs to...
opelresi 4955 ` <. A , A >. ` belongs to...
resres 4956 The restriction of a restr...
resundi 4957 Distributive law for restr...
resundir 4958 Distributive law for restr...
resindi 4959 Class restriction distribu...
resindir 4960 Class restriction distribu...
inres 4961 Move intersection into cla...
resiun1 4962 Distribution of restrictio...
resiun2 4963 Distribution of restrictio...
dmres 4964 The domain of a restrictio...
ssdmres 4965 A domain restricted to a s...
dmresexg 4966 The domain of a restrictio...
resss 4967 A class includes its restr...
rescom 4968 Commutative law for restri...
ssres 4969 Subclass theorem for restr...
ssres2 4970 Subclass theorem for restr...
relres 4971 A restriction is a relatio...
resabs1 4972 Absorption law for restric...
resabs2 4973 Absorption law for restric...
residm 4974 Idempotent law for restric...
resima 4975 A restriction to an image....
resima2 4976 Image under a restricted c...
xpssres 4977 Restriction of a constant ...
elres 4978 Membership in a restrictio...
elsnres 4979 Memebership in restriction...
relssres 4980 Simplification law for res...
resdm 4981 A relation restricted to i...
resexg 4982 The restriction of a set i...
resex 4983 The restriction of a set i...
resopab 4984 Restriction of a class abs...
resiexg 4985 The existence of a restric...
iss 4986 A subclass of the identity...
resopab2 4987 Restriction of a class abs...
resmpt 4988 Restriction of the mapping...
resmpt3 4989 Unconditional restriction ...
dfres2 4990 Alternate definition of th...
opabresid 4991 The restricted identity ex...
mptresid 4992 The restricted identity ex...
dmresi 4993 The domain of a restricted...
resid 4994 Any relation restricted to...
imaeq1 4995 Equality theorem for image...
imaeq2 4996 Equality theorem for image...
imaeq1i 4997 Equality theorem for image...
imaeq2i 4998 Equality theorem for image...
imaeq1d 4999 Equality theorem for image...
imaeq2d 5000 Equality theorem for image...
imaeq12d 5001 Equality theorem for image...
dfima2 5002 Alternate definition of im...
dfima3 5003 Alternate definition of im...
elimag 5004 Membership in an image. T...
elima 5005 Membership in an image. T...
elima2 5006 Membership in an image. T...
elima3 5007 Membership in an image. T...
nfima 5008 Bound-variable hypothesis ...
nfimad 5009 Deduction version of bound...
csbima12g 5010 Move class substitution in...
csbima12gALT 5011 Move class substitution in...
imadmrn 5012 The image of the domain of...
imassrn 5013 The image of a class is a ...
imaexg 5014 The image of a set is a se...
imai 5015 Image under the identity r...
rnresi 5016 The range of the restricte...
resiima 5017 The image of a restriction...
ima0 5018 Image of the empty set. T...
0ima 5019 Image under the empty rela...
imadisj 5020 A class whose image under ...
cnvimass 5021 A preimage under any class...
cnvimarndm 5022 The preimage of the range ...
imasng 5023 The image of a singleton. ...
relimasn 5024 The image of a singleton. ...
elrelimasn 5025 Elementhood in the image o...
elimasn 5026 Membership in an image of ...
elimasng 5027 Membership in an image of ...
elimasni 5028 Membership in an image of ...
args 5029 Two ways to express the cl...
eliniseg 5030 Membership in an initial s...
epini 5031 Any set is equal to its pr...
iniseg 5032 An idiom that signifies an...
dffr3 5033 Alternate definition of we...
dfse2 5034 Alternate definition of se...
exse2 5035 Any set relation is set-li...
imass1 5036 Subset theorem for image. ...
imass2 5037 Subset theorem for image. ...
ndmima 5038 The image of a singleton o...
relcnv 5039 A converse is a relation. ...
relbrcnvg 5040 When ` R ` is a relation, ...
eliniseg2 5041 Eliminate the class existe...
relbrcnv 5042 When ` R ` is a relation, ...
cotr 5043 Two ways of saying a relat...
issref 5044 Two ways to state a relati...
cnvsym 5045 Two ways of saying a relat...
intasym 5046 Two ways of saying a relat...
asymref 5047 Two ways of saying a relat...
asymref2 5048 Two ways of saying a relat...
intirr 5049 Two ways of saying a relat...
brcodir 5050 Two ways of saying that tw...
codir 5051 Two ways of saying a relat...
qfto 5052 A quantifier-free way of e...
xpidtr 5053 A square cross product ` (...
trin2 5054 The intersection of two tr...
poirr2 5055 A partial order relation i...
trinxp 5056 The relation induced by a ...
soirri 5057 A strict order relation is...
sotri 5058 A strict order relation is...
son2lpi 5059 A strict order relation ha...
sotri2 5060 A transitivity relation. ...
sotri3 5061 A transitivity relation. ...
soirriOLD 5062 A strict order relation is...
sotriOLD 5063 A strict order relation is...
son2lpiOLD 5064 A strict order relation ha...
poleloe 5065 Express "less than or equa...
poltletr 5066 Transitive law for general...
somin1 5067 Property of a minimum in a...
somincom 5068 Commutativity of minimum i...
somin2 5069 Property of a minimum in a...
soltmin 5070 Being less than a minimum,...
cnvopab 5071 The converse of a class ab...
cnv0 5072 The converse of the empty ...
cnvi 5073 The converse of the identi...
cnvun 5074 The converse of a union is...
cnvdif 5075 Distributive law for conve...
cnvin 5076 Distributive law for conve...
rnun 5077 Distributive law for range...
rnin 5078 The range of an intersecti...
rniun 5079 The range of an indexed un...
rnuni 5080 The range of a union. Par...
imaundi 5081 Distributive law for image...
imaundir 5082 The image of a union. (Co...
dminss 5083 An upper bound for interse...
imainss 5084 An upper bound for interse...
cnvxp 5085 The converse of a cross pr...
xp0 5086 The cross product with the...
xpnz 5087 The cross product of nonem...
xpeq0 5088 At least one member of an ...
xpdisj1 5089 Cross products with disjoi...
xpdisj2 5090 Cross products with disjoi...
xpsndisj 5091 Cross products with two di...
djudisj 5092 Disjoint unions with disjo...
resdisj 5093 A double restriction to di...
rnxp 5094 The range of a cross produ...
dmxpss 5095 The domain of a cross prod...
rnxpss 5096 The range of a cross produ...
rnxpid 5097 The range of a square cros...
ssxpb 5098 A cross-product subclass r...
xp11 5099 The cross product of non-e...
xpcan 5100 Cancellation law for cross...
xpcan2 5101 Cancellation law for cross...
xpexr 5102 If a cross product is a se...
xpexr2 5103 If a nonempty cross produc...
ssrnres 5104 Subset of the range of a r...
rninxp 5105 Range of the intersection ...
dminxp 5106 Domain of the intersection...
imainrect 5107 Image of a relation restri...
sossfld 5108 The base set of a strict o...
sofld 5109 The base set of a nonempty...
soex 5110 If the relation in a stric...
cnvcnv3 5111 The set of all ordered pai...
dfrel2 5112 Alternate definition of re...
dfrel4v 5113 A relation can be expresse...
cnvcnv 5114 The double converse of a c...
cnvcnv2 5115 The double converse of a c...
cnvcnvss 5116 The double converse of a c...
cnveqb 5117 Equality theorem for conve...
dfrel3 5118 Alternate definition of re...
dmresv 5119 The domain of a universal ...
rnresv 5120 The range of a universal r...
dfrn4 5121 Range defined in terms of ...
rescnvcnv 5122 The restriction of the dou...
cnvcnvres 5123 The double converse of the...
imacnvcnv 5124 The image of the double co...
dmsnn0 5125 The domain of a singleton ...
rnsnn0 5126 The range of a singleton i...
dmsn0 5127 The domain of the singleto...
cnvsn0 5128 The converse of the single...
dmsn0el 5129 The domain of a singleton ...
relsn2 5130 A singleton is a relation ...
dmsnopg 5131 The domain of a singleton ...
dmsnopss 5132 The domain of a singleton ...
dmpropg 5133 The domain of an unordered...
dmsnop 5134 The domain of a singleton ...
dmprop 5135 The domain of an unordered...
dmtpop 5136 The domain of an unordered...
cnvcnvsn 5137 Double converse of a singl...
dmsnsnsn 5138 The domain of the singleto...
rnsnopg 5139 The range of a singleton o...
rnsnop 5140 The range of a singleton o...
op1sta 5141 Extract the first member o...
cnvsn 5142 Converse of a singleton of...
op2ndb 5143 Extract the second member ...
op2nda 5144 Extract the second member ...
cnvsng 5145 Converse of a singleton of...
opswap 5146 Swap the members of an ord...
elxp4 5147 Membership in a cross prod...
elxp5 5148 Membership in a cross prod...
cnvresima 5149 An image under the convers...
resdm2 5150 A class restricted to its ...
resdmres 5151 Restriction to the domain ...
imadmres 5152 The image of the domain of...
mptpreima 5153 The preimage of a function...
mptiniseg 5154 Converse singleton image o...
dmmpt 5155 The domain of the mapping ...
dmmptss 5156 The domain of a mapping is...
dmmptg 5157 The domain of the mapping ...
relco 5158 A composition is a relatio...
dfco2 5159 Alternate definition of a ...
dfco2a 5160 Generalization of ~ dfco2 ...
coundi 5161 Class composition distribu...
coundir 5162 Class composition distribu...
cores 5163 Restricted first member of...
resco 5164 Associative law for the re...
imaco 5165 Image of the composition o...
rnco 5166 The range of the compositi...
rnco2 5167 The range of the compositi...
dmco 5168 The domain of a compositio...
coiun 5169 Composition with an indexe...
cocnvcnv1 5170 A composition is not affec...
cocnvcnv2 5171 A composition is not affec...
cores2 5172 Absorption of a reverse (p...
co02 5173 Composition with the empty...
co01 5174 Composition with the empty...
coi1 5175 Composition with the ident...
coi2 5176 Composition with the ident...
coires1 5177 Composition with a restric...
coass 5178 Associative law for class ...
relcnvtr 5179 A relation is transitive i...
relssdmrn 5180 A relation is included in ...
cnvssrndm 5181 The converse is a subset o...
cossxp 5182 Composition as a subset of...
relrelss 5183 Two ways to describe the s...
unielrel 5184 The membership relation fo...
relfld 5185 The double union of a rela...
relresfld 5186 Restriction of a relation ...
relcoi2 5187 Composition with the ident...
relcoi1 5188 Composition with the ident...
unidmrn 5189 The double union of the co...
relcnvfld 5190 if ` R ` is a relation, it...
dfdm2 5191 Alternate definition of do...
unixp 5192 The double class union of ...
unixp0 5193 A cross product is empty i...
unixpid 5194 Field of a square cross pr...
cnvexg 5195 The converse of a set is a...
cnvex 5196 The converse of a set is a...
relcnvexb 5197 A relation is a set iff it...
ressn 5198 Restriction of a class to ...
cnviin 5199 The converse of an interse...
cnvpo 5200 The converse of a partial ...
cnvso 5201 The converse of a strict o...
coexg 5202 The composition of two set...
coex 5203 The composition of two set...
dffun2 5204 Alternate definition of a ...
dffun3 5205 Alternate definition of fu...
dffun4 5206 Alternate definition of a ...
dffun5 5207 Alternate definition of fu...
dffun6f 5208 Definition of function, us...
dffun6 5209 Alternate definition of a ...
funmo 5210 A function has at most one...
funrel 5211 A function is a relation. ...
funss 5212 Subclass theorem for funct...
funeq 5213 Equality theorem for funct...
funeqi 5214 Equality inference for the...
funeqd 5215 Equality deduction for the...
nffun 5216 Bound-variable hypothesis ...
funeu 5217 There is exactly one value...
funeu2 5218 There is exactly one value...
dffun7 5219 Alternate definition of a ...
dffun8 5220 Alternate definition of a ...
dffun9 5221 Alternate definition of a ...
funfn 5222 An equivalence for the fun...
funi 5223 The identity relation is a...
nfunv 5224 The universe is not a func...
funopg 5225 A Kuratowski ordered pair ...
funopab 5226 A class of ordered pairs i...
funopabeq 5227 A class of ordered pairs o...
funopab4 5228 A class of ordered pairs o...
funmpt 5229 A function in maps-to nota...
funco 5230 The composition of two fun...
funres 5231 A restriction of a functio...
funssres 5232 The restriction of a funct...
fun2ssres 5233 Equality of restrictions o...
funun 5234 The union of functions wit...
funcnvsn 5235 The converse singleton of ...
funsng 5236 A singleton of an ordered ...
fnsng 5237 Functionality and domain o...
funsn 5238 A singleton of an ordered ...
funprg 5239 A set of two pairs is a fu...
funpr 5240 A function with a domain o...
funtp 5241 A function with a domain o...
fnsn 5242 Functionality and domain o...
fnprg 5243 Domain of a function with ...
fntp 5244 A function with a domain o...
fun0 5245 The empty set is a functio...
funcnvcnv 5246 The double converse of a f...
funcnv2 5247 A simpler equivalence for ...
funcnv 5248 The converse of a class is...
funcnv3 5249 A condition showing a clas...
fun2cnv 5250 The double converse of a c...
svrelfun 5251 A single-valued relation i...
fncnv 5252 Single-rootedness (see ~ f...
fun11 5253 Two ways of stating that `...
fununi 5254 The union of a chain (with...
funcnvuni 5255 The union of a chain (with...
fun11uni 5256 The union of a chain (with...
funin 5257 The intersection with a fu...
funres11 5258 The restriction of a one-t...
funcnvres 5259 The converse of a restrict...
cnvresid 5260 Converse of a restricted i...
funcnvres2 5261 The converse of a restrict...
funimacnv 5262 The image of the preimage ...
funimass1 5263 A kind of contraposition l...
funimass2 5264 A kind of contraposition l...
imadif 5265 The image of a difference ...
imain 5266 The image of an intersecti...
funimaexg 5267 Axiom of Replacement using...
funimaex 5268 The image of a set under a...
isarep1 5269 Part of a study of the Axi...
isarep2 5270 Part of a study of the Axi...
fneq1 5271 Equality theorem for funct...
fneq2 5272 Equality theorem for funct...
fneq1d 5273 Equality deduction for fun...
fneq2d 5274 Equality deduction for fun...
fneq12d 5275 Equality deduction for fun...
fneq1i 5276 Equality inference for fun...
fneq2i 5277 Equality inference for fun...
nffn 5278 Bound-variable hypothesis ...
fnfun 5279 A function with domain is ...
fnrel 5280 A function with domain is ...
fndm 5281 The domain of a function. ...
funfni 5282 Inference to convert a fun...
fndmu 5283 A function has a unique do...
fnbr 5284 The first argument of bina...
fnop 5285 The first argument of an o...
fneu 5286 There is exactly one value...
fneu2 5287 There is exactly one value...
fnun 5288 The union of two functions...
fnunsn 5289 Extension of a function wi...
fnco 5290 Composition of two functio...
fnresdm 5291 A function does not change...
fnresdisj 5292 A function restricted to a...
2elresin 5293 Membership in two function...
fnssresb 5294 Restriction of a function ...
fnssres 5295 Restriction of a function ...
fnresin1 5296 Restriction of a function'...
fnresin2 5297 Restriction of a function'...
fnres 5298 An equivalence for functio...
fnresi 5299 Functionality and domain o...
fnima 5300 The image of a function's ...
fn0 5301 A function with empty doma...
fnimadisj 5302 A class that is disjoint w...
fnimaeq0 5303 Images under a function ne...
dfmpt3 5304 Alternate definition for t...
fnopabg 5305 Functionality and domain o...
fnopab 5306 Functionality and domain o...
mptfng 5307 The maps-to notation defin...
fnmpt 5308 The maps-to notation defin...
mpt0 5309 A mapping operation with e...
fnmpti 5310 Functionality and domain o...
dmmpti 5311 Domain of an ordered-pair ...
mptun 5312 Union of mappings which ar...
feq1 5313 Equality theorem for funct...
feq2 5314 Equality theorem for funct...
feq3 5315 Equality theorem for funct...
feq23 5316 Equality theorem for funct...
feq1d 5317 Equality deduction for fun...
feq2d 5318 Equality deduction for fun...
feq12d 5319 Equality deduction for fun...
feq123d 5320 Equality deduction for fun...
feq1i 5321 Equality inference for fun...
feq2i 5322 Equality inference for fun...
feq23i 5323 Equality inference for fun...
feq23d 5324 Equality deduction for fun...
nff 5325 Bound-variable hypothesis ...
elimf 5326 Eliminate a mapping hypoth...
ffn 5327 A mapping is a function. ...
dffn2 5328 Any function is a mapping ...
ffun 5329 A mapping is a function. ...
frel 5330 A mapping is a relation. ...
fdm 5331 The domain of a mapping. ...
fdmi 5332 The domain of a mapping. ...
frn 5333 The range of a mapping. (...
dffn3 5334 A function maps to its ran...
fss 5335 Expanding the codomain of ...
fco 5336 Composition of two mapping...
fco2 5337 Functionality of a composi...
fssxp 5338 A mapping is a class of or...
fex2 5339 A function with bounded do...
funssxp 5340 Two ways of specifying a p...
ffdm 5341 A mapping is a partial fun...
opelf 5342 The members of an ordered ...
fun 5343 The union of two functions...
fun2 5344 The union of two functions...
fnfco 5345 Composition of two functio...
fssres 5346 Restriction of a function ...
fssres2 5347 Restriction of a restricte...
fresin 5348 An identity for the mappin...
resasplit 5349 If two functions agree on ...
fresaun 5350 The union of two functions...
fresaunres2 5351 From the union of two func...
fresaunres1 5352 From the union of two func...
fcoi1 5353 Composition of a mapping a...
fcoi2 5354 Composition of restricted ...
feu 5355 There is exactly one value...
fcnvres 5356 The converse of a restrict...
fimacnvdisj 5357 The preimage of a class di...
fint 5358 Function into an intersect...
fin 5359 Mapping into an intersecti...
fabexg 5360 Existence of a set of func...
fabex 5361 Existence of a set of func...
dmfex 5362 If a mapping is a set, its...
f0 5363 The empty function. (Cont...
f00 5364 A class is a function with...
fconst 5365 A cross product with a sin...
fconstg 5366 A cross product with a sin...
fnconstg 5367 A cross product with a sin...
fconst6g 5368 Constant function with loo...
fconst6 5369 A constant function as a m...
f1eq1 5370 Equality theorem for one-t...
f1eq2 5371 Equality theorem for one-t...
f1eq3 5372 Equality theorem for one-t...
nff1 5373 Bound-variable hypothesis ...
dff12 5374 Alternate definition of a ...
f1f 5375 A one-to-one mapping is a ...
f1fn 5376 A one-to-one mapping is a ...
f1fun 5377 A one-to-one mapping is a ...
f1rel 5378 A one-to-one onto mapping ...
f1dm 5379 The domain of a one-to-one...
f1ss 5380 A function that is one-to-...
f1ssr 5381 Combine a one-to-one funct...
f1ssres 5382 A function that is one-to-...
f1cnvcnv 5383 Two ways to express that a...
f1co 5384 Composition of one-to-one ...
foeq1 5385 Equality theorem for onto ...
foeq2 5386 Equality theorem for onto ...
foeq3 5387 Equality theorem for onto ...
nffo 5388 Bound-variable hypothesis ...
fof 5389 An onto mapping is a mappi...
fofun 5390 An onto mapping is a funct...
fofn 5391 An onto mapping is a funct...
forn 5392 The codomain of an onto fu...
dffo2 5393 Alternate definition of an...
foima 5394 The image of the domain of...
dffn4 5395 A function maps onto its r...
funforn 5396 A function maps its domain...
fodmrnu 5397 An onto function has uniqu...
fores 5398 Restriction of a function....
foco 5399 Composition of onto functi...
foconst 5400 A nonzero constant functio...
f1oeq1 5401 Equality theorem for one-t...
f1oeq2 5402 Equality theorem for one-t...
f1oeq3 5403 Equality theorem for one-t...
f1oeq23 5404 Equality theorem for one-t...
f1eq123d 5405 Equality deduction for one...
foeq123d 5406 Equality deduction for ont...
f1oeq123d 5407 Equality deduction for one...
nff1o 5408 Bound-variable hypothesis ...
f1of1 5409 A one-to-one onto mapping ...
f1of 5410 A one-to-one onto mapping ...
f1ofn 5411 A one-to-one onto mapping ...
f1ofun 5412 A one-to-one onto mapping ...
f1orel 5413 A one-to-one onto mapping ...
f1odm 5414 The domain of a one-to-one...
dff1o2 5415 Alternate definition of on...
dff1o3 5416 Alternate definition of on...
f1ofo 5417 A one-to-one onto function...
dff1o4 5418 Alternate definition of on...
dff1o5 5419 Alternate definition of on...
f1orn 5420 A one-to-one function maps...
f1f1orn 5421 A one-to-one function maps...
f1oabexg 5422 The class of all 1-1-onto ...
f1ocnv 5423 The converse of a one-to-o...
f1ocnvb 5424 A relation is a one-to-one...
f1ores 5425 The restriction of a one-t...
f1orescnv 5426 The converse of a one-to-o...
f1imacnv 5427 Preimage of an image. (Co...
foimacnv 5428 A reverse version of ~ f1i...
foun 5429 The union of two onto func...
f1oun 5430 The union of two one-to-on...
fun11iun 5431 The union of a chain (with...
resdif 5432 The restriction of a one-t...
resin 5433 The restriction of a one-t...
f1oco 5434 Composition of one-to-one ...
f1cnv 5435 The converse of an injecti...
funcocnv2 5436 Composition with the conve...
fococnv2 5437 The composition of an onto...
f1ococnv2 5438 The composition of a one-t...
f1cocnv2 5439 Composition of an injectiv...
f1ococnv1 5440 The composition of a one-t...
f1cocnv1 5441 Composition of an injectiv...
funcoeqres 5442 Re-express a constraint on...
ffoss 5443 Relationship between a map...
f11o 5444 Relationship between one-t...
f10 5445 The empty set maps one-to-...
f1o00 5446 One-to-one onto mapping of...
fo00 5447 Onto mapping of the empty ...
f1o0 5448 One-to-one onto mapping of...
f1oi 5449 A restriction of the ident...
f1ovi 5450 The identity relation is a...
f1osn 5451 A singleton of an ordered ...
f1osng 5452 A singleton of an ordered ...
f1oprswap 5453 A two-element swap is a bi...
fv2 5454 Alternate definition of fu...
fvprc 5455 A function's value at a pr...
elfv 5456 Membership in a function v...
fveq1 5457 Equality theorem for funct...
fveq2 5458 Equality theorem for funct...
fveq1i 5459 Equality inference for fun...
fveq1d 5460 Equality deduction for fun...
fveq2i 5461 Equality inference for fun...
fveq2d 5462 Equality deduction for fun...
fveq12i 5463 Equality deduction for fun...
fveq12d 5464 Equality deduction for fun...
nffv 5465 Bound-variable hypothesis ...
nffvmpt1 5466 Bound-variable hypothesis ...
nffvd 5467 Deduction version of bound...
csbfv12g 5468 Move class substitution in...
csbfv12gALT 5469 Move class substitution in...
csbfv2g 5470 Move class substitution in...
csbfvg 5471 Substitution for a functio...
fvex 5472 The value of a class exist...
fvif 5473 Move a conditional outside...
fv3 5474 Alternate definition of th...
fvres 5475 The value of a restricted ...
funssfv 5476 The value of a member of t...
tz6.12-1 5477 Function value. Theorem 6...
tz6.12 5478 Function value. Theorem 6...
tz6.12f 5479 Function value, using boun...
tz6.12-2 5480 Function value when ` F ` ...
tz6.12c 5481 Corollary of Theorem 6.12(...
tz6.12i 5482 Corollary of Theorem 6.12(...
fvbr0 5483 Two possibilities for the ...
fvrn0 5484 A function value is a memb...
fvssunirn 5485 The result of a function v...
ndmfv 5486 The value of a class outsi...
ndmfvrcl 5487 Reverse closure law for fu...
elfvdm 5488 If a function value has a ...
elfvex 5489 If a function value has a ...
elfvexd 5490 If a function value is non...
nfvres 5491 The value of a non-member ...
nfunsn 5492 If the restriction of a cl...
fv01 5493 Function value of the empt...
fveqres 5494 Equal values imply equal v...
funbrfv 5495 The second argument of a b...
funopfv 5496 The second element in an o...
fnbrfvb 5497 Equivalence of function va...
fnopfvb 5498 Equivalence of function va...
funbrfvb 5499 Equivalence of function va...
funopfvb 5500 Equivalence of function va...
funbrfv2b 5501 Function value in terms of...
dffn5 5502 Representation of a functi...
fnrnfv 5503 The range of a function ex...
fvelrnb 5504 A member of a function's r...
dfimafn 5505 Alternate definition of th...
dfimafn2 5506 Alternate definition of th...
funimass4 5507 Membership relation for th...
fvelima 5508 Function value in an image...
feqmptd 5509 Deduction form of ~ dffn5 ...
feqresmpt 5510 Express a restricted funct...
dffn5f 5511 Representation of a functi...
fvelimab 5512 Function value in an image...
fvi 5513 The value of the identity ...
fviss 5514 The value of the identity ...
fniinfv 5515 The indexed intersection o...
fnsnfv 5516 Singleton of function valu...
fnimapr 5517 The image of a pair under ...
ssimaex 5518 The existence of a subimag...
ssimaexg 5519 The existence of a subimag...
funfv 5520 A simplified expression fo...
funfv2 5521 The value of a function. ...
funfv2f 5522 The value of a function. ...
fvun 5523 Value of the union of two ...
fvun1 5524 The value of a union when ...
fvun2 5525 The value of a union when ...
dffv2 5526 Alternate definition of fu...
dmfco 5527 Domains of a function comp...
fvco2 5528 Value of a function compos...
fvco 5529 Value of a function compos...
fvco3 5530 Value of a function compos...
fvco4i 5531 Conditions for a compositi...
fvopab3g 5532 Value of a function given ...
fvopab3ig 5533 Value of a function given ...
fvmptg 5534 Value of a function given ...
fvmpti 5535 Value of a function given ...
fvmpt 5536 Value of a function given ...
fvmpts 5537 Value of a function given ...
fvmpt3 5538 Value of a function given ...
fvmpt3i 5539 Value of a function given ...
fvmptd 5540 Deduction version of ~ fvm...
fvmpt2i 5541 Value of a function given ...
fvmpt2 5542 Value of a function given ...
fvmptss 5543 If all the values of the m...
fvmptex 5544 Express a function ` F ` w...
fvmptdf 5545 Alternate deduction versio...
fvmptdv 5546 Alternate deduction versio...
fvmptdv2 5547 Alternate deduction versio...
mpteqb 5548 Bidirectional equality the...
fvmptt 5549 Closed theorem form of ~ f...
fvmptf 5550 Value of a function given ...
fvmptnf 5551 The value of a function gi...
fvmptn 5552 This somewhat non-intuitiv...
fvmptss2 5553 A mapping always evaluates...
fvopab4ndm 5554 Value of a function given ...
fvopab6 5555 Value of a function given ...
eqfnfv 5556 Equality of functions is d...
eqfnfv2 5557 Equality of functions is d...
eqfnfv3 5558 Derive equality of functio...
eqfnfvd 5559 Deduction for equality of ...
eqfnfv2f 5560 Equality of functions is d...
eqfunfv 5561 Equality of functions is d...
fvreseq 5562 Equality of restricted fun...
fndmdif 5563 Two ways to express the lo...
fndmdifcom 5564 The difference set between...
fndmdifeq0 5565 The difference set of two ...
fndmin 5566 Two ways to express the lo...
fneqeql 5567 Two functions are equal if...
fneqeql2 5568 Two functions are equal if...
fnreseql 5569 Two functions are equal on...
chfnrn 5570 The range of a choice func...
funfvop 5571 Ordered pair with function...
funfvbrb 5572 Two ways to say that ` A `...
fvimacnvi 5573 A member of a preimage is ...
fvimacnv 5574 The argument of a function...
funimass3 5575 A kind of contraposition l...
funimass5 5576 A subclass of a preimage i...
funconstss 5577 Two ways of specifying tha...
fvimacnvALT 5578 Another proof of ~ fvimacn...
elpreima 5579 Membership in the preimage...
fniniseg 5580 Membership in the preimage...
fncnvima2 5581 Inverse images under funct...
fniniseg2 5582 Inverse point images under...
fnniniseg2 5583 Support sets of functions ...
rexsupp 5584 Existential quantification...
unpreima 5585 Preimage of a union. (Con...
inpreima 5586 Preimage of an intersectio...
difpreima 5587 Preimage of a difference. ...
respreima 5588 The preimage of a restrict...
iinpreima 5589 Preimage of an intersectio...
intpreima 5590 Preimage of an intersectio...
fimacnv 5591 The preimage of the codoma...
suppss 5592 Show that the support of a...
suppssr 5593 A function is zero outside...
fnopfv 5594 Ordered pair with function...
fvelrn 5595 A function's value belongs...
fnfvelrn 5596 A function's value belongs...
ffvelrn 5597 A function's value belongs...
ffvelrni 5598 A function's value belongs...
ffvelrnda 5599 A function's value belongs...
ffvelrnd 5600 A function's value belongs...
rexrn 5601 Restricted existential qua...
ralrn 5602 Restricted universal quant...
ralrnmpt 5603 A restricted quantifier ov...
rexrnmpt 5604 A restricted quantifier ov...
f0cli 5605 Unconditional closure of a...
dff2 5606 Alternate definition of a ...
dff3 5607 Alternate definition of a ...
dff4 5608 Alternate definition of a ...
dffo3 5609 An onto mapping expressed ...
dffo4 5610 Alternate definition of an...
dffo5 5611 Alternate definition of an...
exfo 5612 A relation equivalent to t...
foelrn 5613 Property of a surjective f...
foco2 5614 If a composition of two fu...
fmpt 5615 Functionality of the mappi...
f1ompt 5616 Express bijection for a ma...
fmpti 5617 Functionality of the mappi...
fmptd 5618 Domain and co-domain of th...
ffnfv 5619 A function maps to a class...
ffnfvf 5620 A function maps to a class...
fnfvrnss 5621 An upper bound for range d...
fmpt2d 5622 Domain and co-domain of th...
fmpt2dOLD 5623 Domain and co-domain of th...
ffvresb 5624 A necessary and sufficient...
fmptco 5625 Composition of two functio...
fmptcof 5626 Version of ~ fmptco where ...
fmptcos 5627 Composition of two functio...
fcompt 5628 Express composition of two...
fcoconst 5629 Composition with a constan...
fsn 5630 A function maps a singleto...
fsng 5631 A function maps a singleto...
fsn2 5632 A function that maps a sin...
xpsng 5633 The cross product of two s...
xpsn 5634 The cross product of two s...
dfmpt 5635 Alternate definition for t...
fnasrn 5636 A function expressed as th...
ressnop0 5637 If ` A ` is not in ` C ` ,...
fpr 5638 A function with a domain o...
fnressn 5639 A function restricted to a...
funressn 5640 A function restricted to a...
fressnfv 5641 The value of a function re...
fvconst 5642 The value of a constant fu...
fmptsn 5643 Express a singleton functi...
fmptap 5644 Append an additional value...
fvresi 5645 The value of a restricted ...
fvunsn 5646 Remove an ordered pair not...
fvsn 5647 The value of a singleton o...
fvsng 5648 The value of a singleton o...
fvsnun1 5649 The value of a function wi...
fvsnun2 5650 The value of a function wi...
fnsnsplit 5651 Split a function into a si...
fsnunf 5652 Adjoining a point to a fun...
fsnunf2 5653 Adjoining a point to a pun...
fsnunfv 5654 Recover the added point fr...
fsnunres 5655 Recover the original funct...
fvpr1 5656 The value of a function wi...
fvpr2 5657 The value of a function wi...
fvtp1 5658 The first value of a funct...
fvtp2 5659 The second value of a func...
fvtp3 5660 The third value of a funct...
fvconst2g 5661 The value of a constant fu...
fconst2g 5662 A constant function expres...
fvconst2 5663 The value of a constant fu...
fconst2 5664 A constant function expres...
fconst5 5665 Two ways to express that a...
fnsuppres 5666 Two ways to express restri...
fnsuppeq0 5667 The support of a function ...
fconstfv 5668 A constant function expres...
fconst3 5669 Two ways to express a cons...
fconst4 5670 Two ways to express a cons...
resfunexg 5671 The restriction of a funct...
resfunexgALT 5672 The restriction of a funct...
cofunexg 5673 Existence of a composition...
cofunex2g 5674 Existence of a composition...
fnex 5675 If the domain of a functio...
fnexALT 5676 If the domain of a functio...
funex 5677 If the domain of a functio...
opabex 5678 Existence of a function ex...
mptexg 5679 If the domain of a functio...
mptex 5680 If the domain of a functio...
funrnex 5681 If the domain of a functio...
zfrep6 5682 A version of the Axiom of ...
fex 5683 If the domain of a mapping...
fornex 5684 If the domain of an onto f...
f1dmex 5685 If the codomain of a one-t...
eufnfv 5686 A function is uniquely det...
funfvima 5687 A function's value in a pr...
funfvima2 5688 A function's value in an i...
funfvima3 5689 A class including a functi...
fnfvima 5690 The function value of an o...
rexima 5691 Existential quantification...
ralima 5692 Universal quantification u...
idref 5693 TODO: This is the same as...
fvclss 5694 Upper bound for the class ...
fvclex 5695 Existence of the class of ...
fvresex 5696 Existence of the class of ...
abrexex 5697 Existence of a class abstr...
abrexexg 5698 Existence of a class abstr...
elabrex 5699 Elementhood in an image se...
abrexco 5700 Composition of two image m...
iunexg 5701 The existence of an indexe...
abrexex2g 5702 Existence of an existentia...
opabex3 5703 Existence of an ordered pa...
iunex 5704 The existence of an indexe...
imaiun 5705 The image of an indexed un...
imauni 5706 The image of a union is th...
fniunfv 5707 The indexed union of a fun...
funiunfv 5708 The indexed union of a fun...
funiunfvf 5709 The indexed union of a fun...
eluniima 5710 Membership in the union of...
elunirn 5711 Membership in the union of...
fnunirn 5712 Membership in a union of s...
elunirnALT 5713 Membership in the union of...
abrexex2 5714 Existence of an existentia...
abexssex 5715 Existence of a class abstr...
abexex 5716 A condition where a class ...
dff13 5717 A one-to-one function in t...
dff13f 5718 A one-to-one function in t...
f1mpt 5719 Express injection for a ma...
f1fveq 5720 Equality of function value...
f1elima 5721 Membership in the image of...
f1imass 5722 Taking images under a one-...
f1imaeq 5723 Taking images under a one-...
f1imapss 5724 Taking images under a one-...
dff1o6 5725 A one-to-one onto function...
f1ocnvfv1 5726 The converse value of the ...
f1ocnvfv2 5727 The value of the converse ...
f1ocnvfv 5728 Relationship between the v...
f1ocnvfvb 5729 Relationship between the v...
f1ocnvdm 5730 The value of the converse ...
fcof1 5731 An application is injectiv...
fcofo 5732 An application is surjecti...
cbvfo 5733 Change bound variable betw...
cbvexfo 5734 Change bound variable betw...
cocan1 5735 An injection is left-cance...
cocan2 5736 A surjection is right-canc...
fcof1o 5737 Show that two functions ar...
foeqcnvco 5738 Condition for function equ...
f1eqcocnv 5739 Condition for function equ...
fveqf1o 5740 Given a bijection ` F ` , ...
fliftrel 5741 ` F ` , a function lift, i...
fliftel 5742 Elementhood in the relatio...
fliftel1 5743 Elementhood in the relatio...
fliftcnv 5744 Converse of the relation `...
fliftfun 5745 The function ` F ` is the ...
fliftfund 5746 The function ` F ` is the ...
fliftfuns 5747 The function ` F ` is the ...
fliftf 5748 The domain and range of th...
fliftval 5749 The value of the function ...
isoeq1 5750 Equality theorem for isomo...
isoeq2 5751 Equality theorem for isomo...
isoeq3 5752 Equality theorem for isomo...
isoeq4 5753 Equality theorem for isomo...
isoeq5 5754 Equality theorem for isomo...
nfiso 5755 Bound-variable hypothesis ...
isof1o 5756 An isomorphism is a one-to...
isorel 5757 An isomorphism connects bi...
soisores 5758 Express the condition of i...
soisoi 5759 Infer isomorphism from one...
isoid 5760 Identity law for isomorphi...
isocnv 5761 Converse law for isomorphi...
isocnv2 5762 Converse law for isomorphi...
isocnv3 5763 Complementation law for is...
isores2 5764 An isomorphism from one we...
isores1 5765 An isomorphism from one we...
isores3 5766 Induced isomorphism on a s...
isotr 5767 Composition (transitive) l...
isomin 5768 Isomorphisms preserve mini...
isoini 5769 Isomorphisms preserve init...
isoini2 5770 Isomorphisms are isomorphi...
isofrlem 5771 Lemma for ~ isofr . (Cont...
isoselem 5772 Lemma for ~ isose . (Cont...
isofr 5773 An isomorphism preserves w...
isose 5774 An isomorphism preserves s...
isofr2 5775 A weak form of ~ isofr tha...
isopolem 5776 Lemma for ~ isopo . (Cont...
isopo 5777 An isomorphism preserves p...
isosolem 5778 Lemma for ~ isoso . (Cont...
isoso 5779 An isomorphism preserves s...
isowe 5780 An isomorphism preserves w...
isowe2 5781 A weak form of ~ isowe tha...
f1oiso 5782 Any one-to-one onto functi...
f1oiso2 5783 Any one-to-one onto functi...
f1owe 5784 Well-ordering of isomorphi...
f1oweALT 5785 Well-ordering of isomorphi...
weniso 5786 A set-like well-ordering h...
weisoeq 5787 Thus there is at most one ...
weisoeq2 5788 Thus there is at most one ...
wemoiso 5789 Thus there is at most one ...
wemoiso2 5790 Thus there is at most one ...
knatar 5791 The Knaster-Tarski theorem...
oveq 5798 Equality theorem for opera...
oveq1 5799 Equality theorem for opera...
oveq2 5800 Equality theorem for opera...
oveq12 5801 Equality theorem for opera...
oveq1i 5802 Equality inference for ope...
oveq2i 5803 Equality inference for ope...
oveq12i 5804 Equality inference for ope...
oveqi 5805 Equality inference for ope...
oveq123i 5806 Equality inference for ope...
oveq1d 5807 Equality deduction for ope...
oveq2d 5808 Equality deduction for ope...
oveqd 5809 Equality deduction for ope...
oveq12d 5810 Equality deduction for ope...
oveqan12d 5811 Equality deduction for ope...
oveqan12rd 5812 Equality deduction for ope...
oveq123d 5813 Equality deduction for ope...
nfovd 5814 Deduction version of bound...
nfov 5815 Bound-variable hypothesis ...
oprabid 5816 The law of concretion. Sp...
ovex 5817 The result of an operation...
ovssunirn 5818 The result of an operation...
ovprc 5819 The value of an operation ...
ovprc1 5820 The value of an operation ...
ovprc2 5821 The value of an operation ...
ovrcl 5822 Reverse closure for an ope...
csbovg 5823 Move class substitution in...
csbov12g 5824 Move class substitution in...
csbov1g 5825 Move class substitution in...
csbov2g 5826 Move class substitution in...
rcla4eov 5827 A frequently used special ...
fnotovb 5828 Equivalence of operation v...
dfoprab2 5829 Class abstraction for oper...
reloprab 5830 An operation class abstrac...
nfoprab1 5831 The abstraction variables ...
nfoprab2 5832 The abstraction variables ...
nfoprab3 5833 The abstraction variables ...
nfoprab 5834 Bound-variable hypothesis ...
oprabbid 5835 Equivalent wff's yield equ...
oprabbidv 5836 Equivalent wff's yield equ...
oprabbii 5837 Equivalent wff's yield equ...
ssoprab2 5838 Equivalence of ordered pai...
ssoprab2b 5839 Equivalence of ordered pai...
eqoprab2b 5840 Equivalence of ordered pai...
mpt2eq123 5841 An equality theorem for th...
mpt2eq12 5842 An equality theorem for th...
mpt2eq123dva 5843 An equality deduction for ...
mpt2eq123dv 5844 An equality deduction for ...
mpt2eq123i 5845 An equality inference for ...
mpt2eq3dva 5846 Slightly more general equa...
mpt2eq3ia 5847 An equality inference for ...
nfmpt21 5848 Bound-variable hypothesis ...
nfmpt22 5849 Bound-variable hypothesis ...
nfmpt2 5850 Bound-variable hypothesis ...
oprab4 5851 Two ways to state the doma...
cbvoprab1 5852 Rule used to change first ...
cbvoprab2 5853 Change the second bound va...
cbvoprab12 5854 Rule used to change first ...
cbvoprab12v 5855 Rule used to change first ...
cbvoprab3 5856 Rule used to change the th...
cbvoprab3v 5857 Rule used to change the th...
cbvmpt2x 5858 Rule to change the bound v...
cbvmpt2 5859 Rule to change the bound v...
cbvmpt2v 5860 Rule to change the bound v...
elimdelov 5861 Eliminate a hypothesis whi...
dmoprab 5862 The domain of an operation...
dmoprabss 5863 The domain of an operation...
rnoprab 5864 The range of an operation ...
rnoprab2 5865 The range of a restricted ...
reldmoprab 5866 The domain of an operation...
oprabss 5867 Structure of an operation ...
eloprabga 5868 The law of concretion for ...
eloprabg 5869 The law of concretion for ...
ssoprab2i 5870 Inference of operation cla...
mpt2v 5871 Operation with universal d...
mpt2mptx 5872 Express a two-argument fun...
mpt2mpt 5873 Express a two-argument fun...
resoprab 5874 Restriction of an operatio...
resoprab2 5875 Restriction of an operator...
resmpt2 5876 Restriction of the mapping...
funoprabg 5877 "At most one" is a suffici...
funoprab 5878 "At most one" is a suffici...
fnoprabg 5879 Functionality and domain o...
mpt2fun 5880 The maps-to notation for a...
fnoprab 5881 Functionality and domain o...
ffnov 5882 An operation maps to a cla...
fovcl 5883 Closure law for an operati...
eqfnov 5884 Equality of two operations...
eqfnov2 5885 Two operators with the sam...
fnov 5886 Representation of a functi...
mpt22eqb 5887 Bidirectional equality the...
rnmpt2 5888 The range of an operation ...
reldmmpt2 5889 The domain of an operation...
elrnmpt2g 5890 Membership in the range of...
elrnmpt2 5891 Membership in the range of...
ralrnmpt2 5892 A restricted quantifier ov...
rexrnmpt2 5893 A restricted quantifier ov...
oprabexd 5894 Existence of an operator a...
oprabex 5895 Existence of an operation ...
oprabex3 5896 Existence of an operation ...
oprabrexex2 5897 Existence of an existentia...
ovid 5898 The value of an operation ...
ovidig 5899 The value of an operation ...
ovidi 5900 The value of an operation ...
ov 5901 The value of an operation ...
ovigg 5902 The value of an operation ...
ovig 5903 The value of an operation ...
ovmpt4g 5904 Value of a function given ...
ovmpt2s 5905 Value of a function given ...
ov2gf 5906 The value of an operation ...
ovmpt2dxf 5907 Value of an operation give...
ovmpt2dx 5908 Value of an operation give...
ovmpt2d 5909 Value of an operation give...
ovmpt2x 5910 The value of an operation ...
ovmpt2ga 5911 Value of an operation give...
ovmpt2a 5912 Value of an operation give...
ovmpt2df 5913 Alternate deduction versio...
ovmpt2dv 5914 Alternate deduction versio...
ovmpt2dv2 5915 Alternate deduction versio...
ovmpt2g 5916 Value of an operation give...
ovmpt2 5917 Value of an operation give...
ov3 5918 The value of an operation ...
ov6g 5919 The value of an operation ...
ovg 5920 The value of an operation ...
ovres 5921 The value of a restricted ...
ovresd 5922 Lemma for converting metri...
oprssov 5923 The value of a member of t...
fovrn 5924 An operation's value belon...
fovrnda 5925 An operation's value belon...
fovrnd 5926 An operation's value belon...
fnrnov 5927 The range of an operation ...
foov 5928 An onto mapping of an oper...
fnovrn 5929 An operation's value belon...
ovelrn 5930 A member of an operation's...
funimassov 5931 Membership relation for th...
ovelimab 5932 Operation value in an imag...
ovconst2 5933 The value of a constant op...
ab2rexex 5934 Existence of a class abstr...
ab2rexex2 5935 Existence of an existentia...
oprssdm 5936 Domain of closure of an op...
ndmovg 5937 The value of an operation ...
ndmov 5938 The value of an operation ...
ndmovcl 5939 The closure of an operatio...
ndmovrcl 5940 Reverse closure law, when ...
ndmovcom 5941 Any operation is commutati...
ndmovass 5942 Any operation is associati...
ndmovdistr 5943 Any operation is distribut...
ndmovord 5944 Elimination of redundant a...
ndmovordi 5945 Elimination of redundant a...
caovclg 5946 Convert an operation closu...
caovcld 5947 Convert an operation closu...
caovcl 5948 Convert an operation closu...
caovcomg 5949 Convert an operation commu...
caovcomd 5950 Convert an operation commu...
caovcom 5951 Convert an operation commu...
caovassg 5952 Convert an operation assoc...
caovassd 5953 Convert an operation assoc...
caovass 5954 Convert an operation assoc...
caovcang 5955 Convert an operation cance...
caovcand 5956 Convert an operation cance...
caovcanrd 5957 Commute the arguments of a...
caovcan 5958 Convert an operation cance...
caovordig 5959 Convert an operation order...
caovordid 5960 Convert an operation order...
caovordg 5961 Convert an operation order...
caovordd 5962 Convert an operation order...
caovord2d 5963 Operation ordering law wit...
caovord3d 5964 Ordering law. (Contribute...
caovord 5965 Convert an operation order...
caovord2 5966 Operation ordering law wit...
caovord3 5967 Ordering law. (Contribute...
caovdig 5968 Convert an operation distr...
caovdid 5969 Convert an operation distr...
caovdir2d 5970 Convert an operation distr...
caovdirg 5971 Convert an operation rever...
caovdird 5972 Convert an operation distr...
caovdi 5973 Convert an operation distr...
caov32d 5974 Rearrange arguments in a c...
caov12d 5975 Rearrange arguments in a c...
caov31d 5976 Rearrange arguments in a c...
caov13d 5977 Rearrange arguments in a c...
caov4d 5978 Rearrange arguments in a c...
caov411d 5979 Rearrange arguments in a c...
caov42d 5980 Rearrange arguments in a c...
caov32 5981 Rearrange arguments in a c...
caov12 5982 Rearrange arguments in a c...
caov31 5983 Rearrange arguments in a c...
caov13 5984 Rearrange arguments in a c...
caov4 5985 Rearrange arguments in a c...
caov411 5986 Rearrange arguments in a c...
caov42 5987 Rearrange arguments in a c...
caovdir 5988 Reverse distributive law. ...
caovdilem 5989 Lemma used by real number ...
caovlem2 5990 Lemma used in real number ...
caovmo 5991 Uniqueness of inverse elem...
grprinvlem 5992 Lemma for ~ grprinvd . (C...
grprinvd 5993 Deduce right inverse from ...
grpridd 5994 Deduce right identity from...
elmpt2cl 5995 If a two-parameter class i...
elmpt2cl1 5996 If a two-parameter class i...
elmpt2cl2 5997 If a two-parameter class i...
elovmpt2 5998 Utility lemma for two-para...
relmptopab 5999 Any function to sets of or...
f1ocnvd 6000 Describe an implicit one-t...
f1od 6001 Describe an implicit one-t...
f1ocnv2d 6002 Describe an implicit one-t...
f1o2d 6003 Describe an implicit one-t...
xpexgALT 6004 The cross product of two s...
f1opw2 6005 A one-to-one mapping induc...
f1opw 6006 A one-to-one mapping induc...
suppss2 6007 Show that the support of a...
suppssfv 6008 Formula building theorem f...
suppssov1 6009 Formula building theorem f...
ofeq 6014 Equality theorem for funct...
ofreq 6015 Equality theorem for funct...
ofexg 6016 A function operation restr...
nfof 6017 Hypothesis builder for fun...
nfofr 6018 Hypothesis builder for fun...
offval 6019 Value of an operation appl...
ofrfval 6020 Value of a relation applie...
ofval 6021 Evaluate a function operat...
ofrval 6022 Exhibit a function relatio...
offn 6023 The function operation pro...
fnfvof 6024 Function value of a pointw...
offval3 6025 General value of ` ( F oF ...
offres 6026 Pointwise combination comm...
off 6027 The function operation pro...
ofres 6028 Restrict the operands of a...
offval2 6029 The function operation exp...
ofrfval2 6030 The function relation acti...
ofco 6031 The composition of a funct...
offveq 6032 Convert an identity of the...
offveqb 6033 Equivalent expressions for...
ofc1 6034 Left operation by a consta...
ofc2 6035 Right operation by a const...
ofc12 6036 Function operation on two ...
caofref 6037 Transfer a reflexive law t...
caofinvl 6038 Transfer a left inverse la...
caofid0l 6039 Transfer a left identity l...
caofid0r 6040 Transfer a right identity ...
caofid1 6041 Transfer a right absorptio...
caofid2 6042 Transfer a right absorptio...
caofcom 6043 Transfer a commutative law...
caofrss 6044 Transfer a relation subset...
caofass 6045 Transfer an associative la...
caoftrn 6046 Transfer a transitivity la...
caofdi 6047 Transfer a distributive la...
caofdir 6048 Transfer a reverse distrib...
caonncan 6049 Transfer ~ nncan -shaped l...
ofmres 6050 Equivalent expressions for...
ofmresval 6051 Value of a restriction of ...
ofmresex 6052 Existence of a restriction...
suppssof1 6053 Formula building theorem f...
1stval 6058 The value of the function ...
2ndval 6059 The value of the function ...
1st0 6060 The value of the first-mem...
2nd0 6061 The value of the second-me...
op1st 6062 Extract the first member o...
op2nd 6063 Extract the second member ...
op1std 6064 Extract the first member o...
op2ndd 6065 Extract the second member ...
op1stg 6066 Extract the first member o...
op2ndg 6067 Extract the second member ...
ot1stg 6068 Extract the first member o...
ot2ndg 6069 Extract the second member ...
ot3rdg 6070 Extract the third member o...
1stval2 6071 Alternate value of the fun...
2ndval2 6072 Alternate value of the fun...
fo1st 6073 The ` 1st ` function maps ...
fo2nd 6074 The ` 2nd ` function maps ...
f1stres 6075 Mapping of a restriction o...
f2ndres 6076 Mapping of a restriction o...
fo1stres 6077 Onto mapping of a restrict...
fo2ndres 6078 Onto mapping of a restrict...
1st2val 6079 Value of an alternate defi...
2nd2val 6080 Value of an alternate defi...
1stcof 6081 Composition of the first m...
2ndcof 6082 Composition of the first m...
xp1st 6083 Location of the first elem...
xp2nd 6084 Location of the second ele...
elxp6 6085 Membership in a cross prod...
elxp7 6086 Membership in a cross prod...
difxp 6087 Difference of Cartesian pr...
difxp1 6088 Difference law for cross p...
difxp2 6089 Difference law for cross p...
eqopi 6090 Equality with an ordered p...
xp2 6091 Representation of cross pr...
unielxp 6092 The membership relation fo...
1st2nd2 6093 Reconstruction of a member...
1st2ndb 6094 Reconstruction of an order...
xpopth 6095 An ordered pair theorem fo...
eqop 6096 Two ways to express equali...
eqop2 6097 Two ways to express equali...
op1steq 6098 Two ways of expressing tha...
2nd1st 6099 Swap the members of an ord...
1st2nd 6100 Reconstruction of a member...
1stdm 6101 The first ordered pair com...
2ndrn 6102 The second ordered pair co...
1st2ndbr 6103 Express an element of a re...
releldm2 6104 Two ways of expressing mem...
reldm 6105 An expression for the doma...
sbcopeq1a 6106 Equality theorem for subst...
csbopeq1a 6107 Equality theorem for subst...
dfopab2 6108 A way to define an ordered...
dfoprab3s 6109 A way to define an operati...
dfoprab3 6110 Operation class abstractio...
dfoprab4 6111 Operation class abstractio...
dfoprab4f 6112 Operation class abstractio...
dfxp3 6113 Define the cross product o...
copsex2gb 6114 Implicit substitution infe...
copsex2ga 6115 Implicit substitution infe...
elopaba 6116 Membership in an ordered p...
exopxfr 6117 Transfer ordered-pair exis...
exopxfr2 6118 Transfer ordered-pair exis...
elopabi 6119 A consequence of membershi...
eloprabi 6120 A consequence of membershi...
mpt2mptsx 6121 Express a two-argument fun...
mpt2mpts 6122 Express a two-argument fun...
dmmpt2ssx 6123 The domain of a mapping is...
fmpt2x 6124 Functionality, domain and ...
fmpt2 6125 Functionality, domain and ...
fnmpt2 6126 Functionality and domain o...
fnmpt2i 6127 Functionality and domain o...
dmmpt2 6128 Domain of a class given by...
mpt2exxg 6129 Existence of an operation ...
mpt2exg 6130 Existence of an operation ...
mpt2exga 6131 If the domain of a functio...
mpt2ex 6132 If the domain of a functio...
mpt20 6133 A mapping operation with e...
ovmptss 6134 If all the values of the m...
relmpt2opab 6135 Any function to sets of or...
fmpt2co 6136 Composition of two functio...
oprabco 6137 Composition of a function ...
oprab2co 6138 Composition of operator ab...
df1st2 6139 An alternate possible defi...
df2nd2 6140 An alternate possible defi...
1stconst 6141 The mapping of a restricti...
2ndconst 6142 The mapping of a restricti...
dfmpt2 6143 Alternate definition for t...
curry1 6144 Composition with ` ``' ( 2...
curry1val 6145 The value of a curried fun...
curry1f 6146 Functionality of a curried...
curry2 6147 Composition with ` ``' ( 1...
curry2f 6148 Functionality of a curried...
curry2val 6149 The value of a curried fun...
cnvf1olem 6150 Lemma for ~ cnvf1o . (Con...
cnvf1o 6151 Describe a function that m...
fparlem1 6152 Lemma for ~ fpar . (Contr...
fparlem2 6153 Lemma for ~ fpar . (Contr...
fparlem3 6154 Lemma for ~ fpar . (Contr...
fparlem4 6155 Lemma for ~ fpar . (Contr...
fpar 6156 Merge two functions in par...
fsplit 6157 A function that can be use...
algrflem 6158 Lemma for ~ algrf and rela...
frxp 6159 A lexicographical ordering...
xporderlem 6160 Lemma for lexicographical ...
poxp 6161 A lexicographical ordering...
soxp 6162 A lexicographical ordering...
wexp 6163 A lexicographical ordering...
fnwelem 6164 Lemma for ~ fnwe . (Contr...
fnwe 6165 A variant on lexicographic...
fnse 6166 Condition for the well-ord...
tposss 6169 Subset theorem for transpo...
tposeq 6170 Equality theorem for trans...
tposeqd 6171 Equality theorem for trans...
tposssxp 6172 The transposition is a sub...
reltpos 6173 The transposition is a rel...
brtpos2 6174 Value of the transposition...
brtpos0 6175 The behavior of ` tpos ` w...
reldmtpos 6176 Necessary and sufficient c...
brtpos 6177 The transposition swaps ar...
ottpos 6178 The transposition swaps th...
relbrtpos 6179 The transposition swaps ar...
dmtpos 6180 The domain of ` tpos F ` w...
rntpos 6181 The range of ` tpos F ` wh...
tposexg 6182 The transposition of a set...
ovtpos 6183 The transposition swaps th...
tposfun 6184 The transposition of a fun...
dftpos2 6185 Alternate definition of ` ...
dftpos3 6186 Alternate definition of ` ...
dftpos4 6187 Alternate definition of ` ...
tpostpos 6188 Value of the double transp...
tpostpos2 6189 Value of the double transp...
tposfn2 6190 The domain of a transposit...
tposfo2 6191 Condition for a surjective...
tposf2 6192 The domain and range of a ...
tposf12 6193 Condition for an injective...
tposf1o2 6194 Condition of a bijective t...
tposfo 6195 The domain and range of a ...
tposf 6196 The domain and range of a ...
tposfn 6197 Functionality of a transpo...
tpos0 6198 Transposition of the empty...
tposco 6199 Transposition of a composi...
tpossym 6200 Two ways to say a function...
tposeqi 6201 Equality theorem for trans...
tposex 6202 A transposition is a set. ...
nftpos 6203 Hypothesis builder for tra...
tposoprab 6204 Transposition of a class o...
tposmpt2 6205 Transposition of a two-arg...
relrpss 6212 The proper subset relation...
brrpssg 6213 The proper subset relation...
brrpss 6214 The proper subset relation...
porpss 6215 Every class is partially o...
sorpss 6216 Express strict ordering un...
sorpssi 6217 Property of a chain of set...
sorpssun 6218