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

Theorem dffr2 4295
 Description: Alternate definition of well-founded relation. Similar to Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof shortened by Mario Carneiro, 23-Jun-2015.)
Assertion
Ref Expression
dffr2
Distinct variable groups:   ,,,   ,,,

Proof of Theorem dffr2
StepHypRef Expression
1 df-fr 4289 . 2
2 rabeq0 3418 . . . . 5
32rexbii 2539 . . . 4
43imbi2i 305 . . 3
54albii 1554 . 2
61, 5bitr4i 245 1
 Colors of variables: wff set class Syntax hints:   wn 5   wi 6   wb 178   wa 360  wal 1532   wceq 1619   wne 2419  wral 2516  wrex 2517  crab 2519   wss 3094  c0 3397   class class class wbr 3963   wfr 4286 This theorem is referenced by:  fr0  4309  dfepfr  4315  dffr3  4998 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2520  df-rex 2521  df-rab 2523  df-v 2742  df-dif 3097  df-nul 3398  df-fr 4289
 Copyright terms: Public domain W3C validator