![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-pred | Structured version Visualization version GIF version |
Description: Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6322). (Contributed by Scott Fenton, 29-Jan-2011.) |
Ref | Expression |
---|---|
df-pred | ⊢ Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋})) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cR | . . 3 class 𝑅 | |
3 | cX | . . 3 class 𝑋 | |
4 | 1, 2, 3 | cpred 6304 | . 2 class Pred(𝑅, 𝐴, 𝑋) |
5 | 2 | ccnv 5676 | . . . 4 class ◡𝑅 |
6 | 3 | csn 4629 | . . . 4 class {𝑋} |
7 | 5, 6 | cima 5680 | . . 3 class (◡𝑅 “ {𝑋}) |
8 | 1, 7 | cin 3944 | . 2 class (𝐴 ∩ (◡𝑅 “ {𝑋})) |
9 | 4, 8 | wceq 1533 | 1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋})) |
Colors of variables: wff setvar class |
This definition is referenced by: predeq123 6306 nfpred 6310 csbpredg 6311 predpredss 6312 predss 6313 sspred 6314 dfpred2 6315 elpredgg 6318 predexg 6323 dffr4 6325 predel 6326 predidm 6332 predin 6333 predun 6334 preddif 6335 predep 6336 pred0 6341 dfse3 6342 predrelss 6343 predprc 6344 predres 6345 frpoind 6348 wfiOLD 6357 frind 9773 |
Copyright terms: Public domain | W3C validator |