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