| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: An abstraction relation is a subset of a related cross product. |
| Ref | Expression |
|---|---|
| opabssxp |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simpl 437 |
. . 3
| |
| 2 | 1 | ssopab2i 3735 |
. 2
|
| 3 | df-xp 4133 |
. 2
| |
| 4 | 2, 3 | sseqtr4i 2877 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: dmoprabss 5025 ecopoprdm 5529 ecopoprsym 5530 ecopoprtrn 5531 enqex 6566 ltrelpq 6569 ltrelpr 6619 enrex 6696 ltrelsr 6698 ltrelre 6770 lmfval 10069 bcthlem12 10154 bcthlem15 10157 dmhmph 15643 rnhmph 15644 tlmval 16727 phtpcval 16882 cmtfval 17604 cvrfval 17660 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1592 ax-gen 1593 ax-8 1594 ax-9 1595 ax-10 1596 ax-11 1597 ax-12 1598 ax-14 1600 ax-17 1605 ax-4 1608 ax-5o 1610 ax-6o 1613 ax-9o 1763 ax-10o 1781 ax-16 1854 ax-11o 1864 ax-ext 2123 ax-sep 3606 ax-nul 3613 ax-pow 3649 ax-pr 3687 |
| This theorem depends on definitions: df-bi 220 df-or 338 df-an 339 df-ex 1616 df-sb 1816 df-eu 2041 df-mo 2042 df-clab 2129 df-cleq 2134 df-clel 2137 df-ne 2268 df-v 2540 df-dif 2830 df-un 2832 df-in 2834 df-ss 2836 df-nul 3083 df-pw 3229 df-sn 3242 df-pr 3243 df-op 3246 df-opab 3566 df-xp 4133 |