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

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