![]() |
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 6339). (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 6321 | . 2 class Pred(𝑅, 𝐴, 𝑋) |
5 | 2 | ccnv 5687 | . . . 4 class ◡𝑅 |
6 | 3 | csn 4630 | . . . 4 class {𝑋} |
7 | 5, 6 | cima 5691 | . . 3 class (◡𝑅 “ {𝑋}) |
8 | 1, 7 | cin 3961 | . 2 class (𝐴 ∩ (◡𝑅 “ {𝑋})) |
9 | 4, 8 | wceq 1536 | 1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋})) |
Colors of variables: wff setvar class |
This definition is referenced by: predeq123 6323 nfpred 6327 csbpredg 6328 predpredss 6329 predss 6330 sspred 6331 dfpred2 6332 elpredgg 6335 predexg 6340 dffr4 6342 predel 6343 predidm 6348 predin 6349 predun 6350 preddif 6351 predep 6352 pred0 6357 dfse3 6358 predrelss 6359 predprc 6360 predres 6361 frpoind 6364 wfiOLD 6373 frind 9787 |
Copyright terms: Public domain | W3C validator |