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

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