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 5610) . (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 5596 | . 2 class Pred(𝑅, 𝐴, 𝑋) |
5 | 2 | ccnv 5037 | . . . 4 class ◡𝑅 |
6 | 3 | csn 4125 | . . . 4 class {𝑋} |
7 | 5, 6 | cima 5041 | . . 3 class (◡𝑅 “ {𝑋}) |
8 | 1, 7 | cin 3539 | . 2 class (𝐴 ∩ (◡𝑅 “ {𝑋})) |
9 | 4, 8 | wceq 1475 | 1 wff Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋})) |
Colors of variables: wff setvar class |
This definition is referenced by: predeq123 5598 nfpred 5602 predpredss 5603 predss 5604 sspred 5605 dfpred2 5606 elpredim 5609 elpred 5610 elpredg 5611 predasetex 5612 dffr4 5613 predel 5614 predidm 5619 predin 5620 predun 5621 preddif 5622 predep 5623 pred0 5627 wfi 5630 frind 30984 csbpredg 32348 |
Copyright terms: Public domain | W3C validator |