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.

Step	Hyp	Ref	Expression
1		df-fr 4843	. . 3
2		sseq1 3524	. . . . . 6
3		neeq1 2738	. . . . . 6
4	2, 3	anbi12d 710	. . . . 5
5		raleq 3054	. . . . . 6
6	5	rexeqbi1dv 3063	. . . . 5
7	4, 6	imbi12d 320	. . . 4
8	7	spcgv 3194	. . 3
9	1, 8	syl5bi 217	. 2
10	9	imp31 432	1

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