![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > eqrelriiv | Structured 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 5036 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2, 4 | mp2an 672 |
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 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1954 ax-ext 2431 ax-sep 4516 ax-nul 4524 ax-pr 4634 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2602 df-ne 2647 df-v 3074 df-dif 3434 df-un 3436 df-in 3438 df-ss 3445 df-nul 3741 df-if 3895 df-sn 3981 df-pr 3983 df-op 3987 df-opab 4454 df-xp 4949 df-rel 4950 |
This theorem is referenced by: eqbrriv 5038 inopab 5073 difopab 5074 dfres2 5261 restidsing 5265 cnvopab 5341 cnv0 5343 cnvdif 5346 difxp 5365 cnvcnvsn 5419 dfco2 5440 coiun 5450 co02 5454 coass 5459 ressn 5476 ovoliunlem1 21112 h2hlm 24529 cnvco1 27709 cnvco2 27710 |
Copyright terms: Public domain | W3C validator |