| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Inference from Theorem 19.21 of [Margaris] p. 90. |
| Ref | Expression |
|---|---|
| 19.21bi.1 |
|
| Ref | Expression |
|---|---|
| 19.21bi |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 19.21bi.1 |
. 2
| |
| 2 | ax-4 1014 |
. 2
| |
| 3 | 1, 2 | syl 10 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: 19.21bbi 1102 aev 1250 2euex 1484 eqeq1 1528 eleq2 1582 r19.21bi 1772 ssel 2114 pocl 2900 funmo 3589 funeu 3594 funun 3611 fn0 3662 hbfvd2 3788 ac7 4810 axpowndlem2 5015 axpowndlem4 5017 axregndlem2 5020 axinfnd 5023 prcdpq 5162 fipfil2 10658 filint2 10665 cmpmon 10825 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-mp 7 ax-4 1014 |