| 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 970 |
. 2
| |
| 2 | a4s.1 |
. 2
| |
| 3 | 1, 2 | syl 10 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: 19.20i 989 19.2 1026 19.21t 1111 exintr 1113 ax10o 1135 cbv1 1158 equvini 1164 drsb1 1171 sbied 1191 ax11v2 1210 dfsb2 1220 sbequi 1223 drsb2 1225 sbn 1226 sbi1 1227 hbsb4 1243 hbsb4t 1244 sbidm 1249 sbco2 1250 sbcom 1253 sbcom2 1329 sbal1 1341 ax11eq 1356 ax11el 1357 ax11inda 1364 a12lem1 1369 mopick 1426 rgen2a 1691 ralcom2 1768 reu3 1921 sbcralt 1980 sbcrext 1981 sbcralgf 1982 sbcrexgf 1983 csbie2t 2023 csbnestg 2026 sbcnestg 2028 moabex 2756 mosubopt 2793 ssopab2 2811 dfid3 2826 alxfr 2886 dmcosseq 3349 fununi 3549 fv3 3718 cbvfo 3870 fnoprabg 3997 pssnn 4513 kmlem16 4752 axextnd 4915 axrepndlem1 4916 axrepndlem2 4917 axunndlem1 4919 axunnd 4920 axpowndlem1 4921 axpowndlem2 4922 axpowndlem3 4923 axpowndlem4 4924 axregndlem1 4926 axregndlem2 4927 axregnd 4928 axinfndlem1 4929 axinfnd 4930 axacndlem4 4934 axacndlem5 4935 axacnd 4936 suppsr3 5196 uninqs 10342 cmphmp 10408 qusp 10430 imonclem 10583 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-mp 7 ax-4 970 |