![]() |
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 relationship. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 5852) . (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 5838 | . 2 class Pred(𝑅, 𝐴, 𝑋) |
5 | 2 | ccnv 5263 | . . . 4 class ◡𝑅 |
6 | 3 | csn 4319 | . . . 4 class {𝑋} |
7 | 5, 6 | cima 5267 | . . 3 class (◡𝑅 “ {𝑋}) |
8 | 1, 7 | cin 3712 | . 2 class (𝐴 ∩ (◡𝑅 “ {𝑋})) |
9 | 4, 8 | wceq 1630 | 1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋})) |
Colors of variables: wff setvar class |
This definition is referenced by: predeq123 5840 nfpred 5844 predpredss 5845 predss 5846 sspred 5847 dfpred2 5848 elpredim 5851 elpred 5852 elpredg 5853 predasetex 5854 dffr4 5855 predel 5856 predidm 5861 predin 5862 predun 5863 preddif 5864 predep 5865 pred0 5869 wfi 5872 frpoind 32044 frind 32047 csbpredg 33481 |
Copyright terms: Public domain | W3C validator |