| 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 6338). (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 6320 | . 2 class Pred(𝑅, 𝐴, 𝑋) |
| 5 | 2 | ccnv 5684 | . . . 4 class ◡𝑅 |
| 6 | 3 | csn 4626 | . . . 4 class {𝑋} |
| 7 | 5, 6 | cima 5688 | . . 3 class (◡𝑅 “ {𝑋}) |
| 8 | 1, 7 | cin 3950 | . 2 class (𝐴 ∩ (◡𝑅 “ {𝑋})) |
| 9 | 4, 8 | wceq 1540 | 1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋})) |
| Colors of variables: wff setvar class |
| This definition is referenced by: predeq123 6322 nfpred 6326 csbpredg 6327 predpredss 6328 predss 6329 sspred 6330 dfpred2 6331 elpredgg 6334 predexg 6339 dffr4 6341 predel 6342 predidm 6347 predin 6348 predun 6349 preddif 6350 predep 6351 pred0 6356 dfse3 6357 predrelss 6358 predprc 6359 predres 6360 frpoind 6363 wfiOLD 6372 frind 9790 |
| Copyright terms: Public domain | W3C validator |