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 6155) . (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 6141 | . 2 class Pred(𝑅, 𝐴, 𝑋) |
5 | 2 | ccnv 5548 | . . . 4 class ◡𝑅 |
6 | 3 | csn 4559 | . . . 4 class {𝑋} |
7 | 5, 6 | cima 5552 | . . 3 class (◡𝑅 “ {𝑋}) |
8 | 1, 7 | cin 3934 | . 2 class (𝐴 ∩ (◡𝑅 “ {𝑋})) |
9 | 4, 8 | wceq 1528 | 1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋})) |
Colors of variables: wff setvar class |
This definition is referenced by: predeq123 6143 nfpred 6147 predpredss 6148 predss 6149 sspred 6150 dfpred2 6151 elpredim 6154 elpred 6155 elpredg 6156 predasetex 6157 dffr4 6158 predel 6159 predidm 6164 predin 6165 predun 6166 preddif 6167 predep 6168 pred0 6172 wfi 6175 frpoind 32978 frind 32983 csbpredg 34490 |
Copyright terms: Public domain | W3C validator |