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

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

Proof of Theorem fri
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 df-fr 4843 . . 3
2 sseq1 3524 . . . . . 6
3 neeq1 2738 . . . . . 6
42, 3anbi12d 710 . . . . 5
5 raleq 3054 . . . . . 6
65rexeqbi1dv 3063 . . . . 5
74, 6imbi12d 320 . . . 4
87spcgv 3194 . . 3
91, 8syl5bi 217 . 2
109imp31 432 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  /\wa 369  A.wal 1393  =wceq 1395  e.wcel 1818  =/=wne 2652  A.wral 2807  E.wrex 2808  C_wss 3475   c0 3784   class class class wbr 4452  Frwfr 4840
This theorem is referenced by:  frc  4850  fr2nr  4862  frminex  4864  wereu  4880  wereu2  4881  fr3nr  6615  frfi  7785  fimax2g  7786  wofib  7991  wemapso  7997  wemapso2OLD  7998  wemapso2lem  7999  noinfep  8097  noinfepOLD  8098  cflim2  8664  isfin1-3  8787  fin12  8814  fpwwe2lem12  9040  fpwwe2lem13  9041  fpwwe2  9042  frinfm  30226  fdc  30238  fnwe2lem2  30997  bnj110  33916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-v 3111  df-in 3482  df-ss 3489  df-fr 4843
  Copyright terms: Public domain W3C validator