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 6161) . (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 6147 | . 2 class Pred(𝑅, 𝐴, 𝑋) |
5 | 2 | ccnv 5554 | . . . 4 class ◡𝑅 |
6 | 3 | csn 4567 | . . . 4 class {𝑋} |
7 | 5, 6 | cima 5558 | . . 3 class (◡𝑅 “ {𝑋}) |
8 | 1, 7 | cin 3935 | . 2 class (𝐴 ∩ (◡𝑅 “ {𝑋})) |
9 | 4, 8 | wceq 1537 | 1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋})) |
Colors of variables: wff setvar class |
This definition is referenced by: predeq123 6149 nfpred 6153 predpredss 6154 predss 6155 sspred 6156 dfpred2 6157 elpredim 6160 elpred 6161 elpredg 6162 predasetex 6163 dffr4 6164 predel 6165 predidm 6170 predin 6171 predun 6172 preddif 6173 predep 6174 pred0 6178 wfi 6181 frpoind 33080 frind 33085 csbpredg 34610 |
Copyright terms: Public domain | W3C validator |