Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  intirr Unicode version

Theorem intirr 5063
 Description: Two ways of saying a relation is irreflexive. Definition of irreflexivity in [Schechter] p. 51. (Contributed by NM, 9-Sep-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Assertion
Ref Expression
intirr
Distinct variable group:   ,

Proof of Theorem intirr
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 incom 3363 . . . 4
21eqeq1i 2292 . . 3
3 disj2 3504 . . 3
4 reli 4815 . . . 4
5 ssrel 4778 . . . 4
64, 5ax-mp 8 . . 3
72, 3, 63bitri 262 . 2
8 eqcom 2287 . . . . 5
9 vex 2793 . . . . . 6
109ideq 4838 . . . . 5
11 df-br 4026 . . . . 5
128, 10, 113bitr2i 264 . . . 4
13 opex 4239 . . . . . . 7
1413biantrur 492 . . . . . 6
15 eldif 3164 . . . . . 6
1614, 15bitr4i 243 . . . . 5
17 df-br 4026 . . . . 5
1816, 17xchnxbir 300 . . . 4
1912, 18imbi12i 316 . . 3
20192albii 1556 . 2
21 nfv 1607 . . . 4
22 breq2 4029 . . . . 5
2322notbid 285 . . . 4
2421, 23equsal 1902 . . 3
2524albii 1555 . 2
267, 20, 253bitr2i 264 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176   wa 358  wal 1529   wceq 1625   wcel 1686  cvv 2790   cdif 3151   cin 3153   wss 3154  c0 3457  cop 3645   class class class wbr 4025   cid 4306   wrel 4696 This theorem is referenced by:  hartogslem1  7259  hausdiag  17341 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4216 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026  df-opab 4080  df-id 4311  df-xp 4697  df-rel 4698
 Copyright terms: Public domain W3C validator