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

Theorem intirr 5215
 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 3497 . . . 4
21eqeq1i 2415 . . 3
3 disj2 3639 . . 3
4 reli 4965 . . . 4
5 ssrel 4927 . . . 4
64, 5ax-mp 8 . . 3
72, 3, 63bitri 263 . 2
8 equcom 1688 . . . . 5
9 vex 2923 . . . . . 6
109ideq 4988 . . . . 5
11 df-br 4177 . . . . 5
128, 10, 113bitr2i 265 . . . 4
13 opex 4391 . . . . . . 7
1413biantrur 493 . . . . . 6
15 eldif 3294 . . . . . 6
1614, 15bitr4i 244 . . . . 5
17 df-br 4177 . . . . 5
1816, 17xchnxbir 301 . . . 4
1912, 18imbi12i 317 . . 3
20192albii 1573 . 2
21 nfv 1626 . . . 4
22 breq2 4180 . . . . 5
2322notbid 286 . . . 4
2421, 23equsal 1966 . . 3
2524albii 1572 . 2
267, 20, 253bitr2i 265 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wa 359  wal 1546   wceq 1649   wcel 1721  cvv 2920   cdif 3281   cin 3283   wss 3284  c0 3592  cop 3781   class class class wbr 4176   cid 4457   wrel 4846 This theorem is referenced by:  hartogslem1  7471  hausdiag  17634 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pr 4367 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-br 4177  df-opab 4231  df-id 4462  df-xp 4847  df-rel 4848
 Copyright terms: Public domain W3C validator