| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Generalization of antecedent. |
| Ref | Expression |
|---|---|
| a4s.1 |
|
| Ref | Expression |
|---|---|
| a4s |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-4 1608 |
. 2
| |
| 2 | a4s.1 |
. 2
| |
| 3 | 1, 2 | syl 13 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: alimi 1627 19.2 1666 19.21t 1755 exintr 1757 ax10o 1780 cbv1 1804 equveli 1812 drsb1 1819 ax11v2 1861 dfsb2 1871 sbequi 1874 drsb2 1876 sbn 1877 sbi1 1878 sbf3t 1894 hbsb4 1895 hbsb4t 1896 sbco2 1902 sbcom 1905 sbcom2 1990 sbal1 2001 ax11eq 2018 ax11el 2019 ax11inda 2026 a12lem1 2031 eujustALT 2040 mopick 2094 eupickbi 2098 ralcom2 2490 ceqsalg 2562 cla4gft 2601 reu6 2689 sbcralt 2759 sbcrext 2760 sbcralgf 2761 sbcrexgf 2762 csbie2t 2809 csbnestg 2812 sbcnestg 2814 reldisj 3121 moabex 3676 mosubopt 3714 ssopab2 3734 dfid3 3748 alxfr 3982 fununi 4582 fv3 4779 cbvfo 4956 fnoprabg 5034 pssnn 5834 kmlem16 6352 axextnd 6461 axrepndlem1 6462 axrepndlem2 6463 axunndlem1 6465 axunnd 6466 axpowndlem1 6467 axpowndlem2 6468 axpowndlem3 6469 axpowndlem4 6470 axregndlem1 6472 axregndlem2 6473 axregnd 6474 axinfndlem1 6475 axinfnd 6476 axacndlem4 6480 axacndlem5 6481 axacnd 6482 suppsr3 6742 bnj9 13175 fundmpss 14467 wfrlem5 14614 frrlem5 14638 nalf 14853 uninqs 15048 ref4w 15080 pospos 15374 cmphmp 15635 qusp 15671 bwt2 15738 imonclem 15956 pm10.55 17140 2albi 17154 pm11.57 17170 ax4567to6 17186 ax10ext 17188 ax10-16 17189 pm14.122b 17211 pm14.123b 17214 eupickbiOLD 17224 cla4gftOLD 17230 dropab1 17248 dropab2 17249 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-mp 7 ax-4 1608 |