![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqrelriiv | Structured version Visualization version Unicode version |
Description: Inference from extensionality principle for relations. (Contributed by NM, 17-Mar-1995.) |
Ref | Expression |
---|---|
eqreliiv.1 |
![]() ![]() ![]() |
eqreliiv.2 |
![]() ![]() ![]() |
eqreliiv.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eqrelriiv |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqreliiv.1 |
. 2
![]() ![]() ![]() | |
2 | eqreliiv.2 |
. 2
![]() ![]() ![]() | |
3 | eqreliiv.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | eqrelriv 4927 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2, 4 | mp2an 677 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-sep 4524 ax-nul 4533 ax-pr 4638 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-v 3046 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-nul 3731 df-if 3881 df-sn 3968 df-pr 3970 df-op 3974 df-opab 4461 df-xp 4839 df-rel 4840 |
This theorem is referenced by: eqbrriv 4929 inopab 4964 difopab 4965 dfres2 5156 restidsing 5160 cnvopab 5236 cnv0 5238 cnvdif 5241 difxp 5260 cnvcnvsn 5312 dfco2 5333 coiun 5344 co02 5348 coass 5353 ressn 5371 ovoliunlem1 22448 h2hlm 26626 cnvco1 30393 cnvco2 30394 cnviun 36236 coiun1 36238 |
Copyright terms: Public domain | W3C validator |