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