Definition df-pred 5680

Description: Define the predecessor class of a relationship. This is the class of all elements y of A such that y R X (see elpred 5693) . (Contributed by Scott Fenton, 29-Jan-2011.)

Assertion

Ref	Expression
df-pred	|- Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) )

Detailed syntax breakdown of Definition df-pred

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3		cX	. . 3 class X
4	1, 2, 3	cpred 5679	. 2 class Pred ( R , A , X )
5	2	ccnv 5113	. . . 4 class `' R
6	3	csn 4177	. . . 4 class { X }
7	5, 6	cima 5117	. . 3 class ( `' R " { X } )
8	1, 7	cin 3573	. 2 class ( A i^i ( `' R " { X } ) )
9	4, 8	wceq 1483	1 wff Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) )

This definition is referenced by:  predeq123  5681  nfpred  5685  predpredss  5686  predss  5687  sspred  5688  dfpred2  5689  elpredim  5692  elpred  5693  elpredg  5694  predasetex  5695  dffr4  5696  predel  5697  predidm  5702  predin  5703  predun  5704  preddif  5705  predep  5706  pred0  5710  wfi  5713  frind  31740  csbpredg  33172