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 6217). (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 6199 | . 2 class Pred(𝑅, 𝐴, 𝑋) |
5 | 2 | ccnv 5588 | . . . 4 class ◡𝑅 |
6 | 3 | csn 4567 | . . . 4 class {𝑋} |
7 | 5, 6 | cima 5592 | . . 3 class (◡𝑅 “ {𝑋}) |
8 | 1, 7 | cin 3891 | . 2 class (𝐴 ∩ (◡𝑅 “ {𝑋})) |
9 | 4, 8 | wceq 1542 | 1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋})) |
Colors of variables: wff setvar class |
This definition is referenced by: predeq123 6201 nfpred 6205 csbpredg 6206 predpredss 6207 predss 6208 sspred 6209 dfpred2 6210 elpredgg 6213 predexg 6218 dffr4 6220 predel 6221 predidm 6227 predin 6228 predun 6229 preddif 6230 predep 6231 pred0 6236 dfse3 6237 predrelss 6238 predprc 6239 predres 6240 frpoind 6243 wfiOLD 6252 frind 9501 |
Copyright terms: Public domain | W3C validator |