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