![]() |
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 6324). (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 6306 | . 2 class Pred(𝑅, 𝐴, 𝑋) |
5 | 2 | ccnv 5677 | . . . 4 class ◡𝑅 |
6 | 3 | csn 4630 | . . . 4 class {𝑋} |
7 | 5, 6 | cima 5681 | . . 3 class (◡𝑅 “ {𝑋}) |
8 | 1, 7 | cin 3943 | . 2 class (𝐴 ∩ (◡𝑅 “ {𝑋})) |
9 | 4, 8 | wceq 1533 | 1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋})) |
Colors of variables: wff setvar class |
This definition is referenced by: predeq123 6308 nfpred 6312 csbpredg 6313 predpredss 6314 predss 6315 sspred 6316 dfpred2 6317 elpredgg 6320 predexg 6325 dffr4 6327 predel 6328 predidm 6334 predin 6335 predun 6336 preddif 6337 predep 6338 pred0 6343 dfse3 6344 predrelss 6345 predprc 6346 predres 6347 frpoind 6350 wfiOLD 6359 frind 9775 |
Copyright terms: Public domain | W3C validator |