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

Theorem fri 4841
 Description: Property of well-founded relation (one direction of definition). (Contributed by NM, 18-Mar-1997.)
Assertion
Ref Expression
fri
Distinct variable groups:   ,,   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem fri
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 df-fr 4838 . . 3
2 sseq1 3525 . . . . . 6
3 neeq1 2748 . . . . . 6
42, 3anbi12d 710 . . . . 5
5 raleq 3058 . . . . . 6
65rexeqbi1dv 3067 . . . . 5
74, 6imbi12d 320 . . . 4
87spcgv 3198 . . 3
91, 8syl5bi 217 . 2
109imp31 432 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wa 369  wal 1377   wceq 1379   wcel 1767   wne 2662  wral 2814  wrex 2815   wss 3476  c0 3785   class class class wbr 4447   wfr 4835 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-v 3115  df-in 3483  df-ss 3490  df-fr 4838 This theorem is referenced by:  frc  4845  fr2nr  4857  frminex  4859  wereu  4875  wereu2  4876  fr3nr  6599  frfi  7765  fimax2g  7766  wofib  7970  wemapso  7976  wemapso2OLD  7977  wemapso2lem  7978  noinfep  8076  noinfepOLD  8077  cflim2  8643  isfin1-3  8766  fin12  8793  fpwwe2lem12  9019  fpwwe2lem13  9020  fpwwe2  9021  frinfm  29857  fdc  29869  fnwe2lem2  30629  bnj110  33013
 Copyright terms: Public domain W3C validator