New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > albii | GIF version |
Description: Inference adding universal quantifier to both sides of an equivalence. (Contributed by NM, 7-Aug-1994.) |
Ref | Expression |
---|---|
albii.1 | ⊢ (φ ↔ ψ) |
Ref | Expression |
---|---|
albii | ⊢ (∀xφ ↔ ∀xψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | albi 1564 | . 2 ⊢ (∀x(φ ↔ ψ) → (∀xφ ↔ ∀xψ)) | |
2 | albii.1 | . 2 ⊢ (φ ↔ ψ) | |
3 | 1, 2 | mpg 1548 | 1 ⊢ (∀xφ ↔ ∀xψ) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 176 ∀wal 1540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 |
This theorem depends on definitions: df-bi 177 |
This theorem is referenced by: 2albii 1567 hbxfrbi 1568 nfbii 1569 alex 1572 2nalexn 1573 alinexa 1578 alexn 1579 19.26-2 1594 19.26-3an 1595 19.35 1600 19.30 1604 19.43OLD 1606 albiim 1611 2albiim 1612 exintrbi 1613 19.8wOLD 1693 alrot3 1738 alrot4 1739 hba1 1786 equsalhw 1838 equsalhwOLD 1839 dvelimhw 1849 19.21-2 1864 19.32 1875 19.31 1876 aaan 1884 19.23vv 1892 pm11.53 1893 19.12vv 1898 ax12olem2 1928 equsal 1960 dvelimh 1964 sbcom 2089 sb8e 2093 sbnf2 2108 2sb6 2113 sbcom2 2114 sb6a 2116 2sb6rf 2118 sbex 2128 sbalv 2129 2exsb 2132 dvelimALT 2133 sbal2 2134 dvelimf-o 2180 ax10-16 2190 sb8eu 2222 eu1 2225 eu2 2229 moanim 2260 2mo 2282 2eu3 2286 2eu4 2287 exists1 2293 eqcom 2355 hblem 2457 abeq2 2458 abeq1 2459 nfceqi 2485 abid2f 2514 ralbii2 2642 r2alf 2649 r3al 2671 r19.21t 2699 r19.23t 2728 rabid2 2788 rabbi 2789 ralv 2872 ceqsralt 2882 ralab 2997 ralrab2 3002 euind 3023 reu2 3024 reu3 3026 rmo4 3029 reu8 3032 rmoim 3035 2reuswap 3038 reuind 3039 2reu5lem2 3042 2reu5lem3 3043 ra5 3130 rmo2 3131 rmo3 3133 dfss2 3262 ss2ab 3334 ss2rab 3342 rabss 3343 uniiunlem 3353 ssequn1 3433 unss 3437 ralunb 3444 ssin 3477 n0f 3558 eqv 3565 disj 3591 disj3 3595 ssdif0 3609 inssdif0 3617 ssundif 3633 sscon34 3661 pwss 3736 ralsns 3763 disjsn 3786 euabsn2 3791 snss 3838 pwpw0 3855 pwsnALT 3882 dfnfc2 3909 unissb 3921 elintrab 3938 ssintrab 3949 intun 3958 intpr 3959 dfiin2g 4000 iunss 4007 axprimlem1 4088 axprimlem2 4089 axxpprim 4090 axsiprim 4093 axtyplowerprim 4094 axins2prim 4095 axins3prim 4096 ninexg 4097 1cex 4142 eqpw1 4162 pw111 4170 ssrelk 4211 eqrelk 4212 elp6 4263 xpkvexg 4285 p6exg 4290 dfuni12 4291 sikexlem 4295 dfimak2 4298 insklem 4304 ins2kexg 4305 ins3kexg 4306 sb8iota 4346 ssfin 4470 nnadjoin 4520 nnadjoinpw 4521 nnpweq 4523 tfinnn 4534 spfininduct 4540 eqop 4611 raliunxp 4823 ssopr 4846 eqopr 4847 dmopab3 4917 dm0rn0 4921 dmeq0 4922 cotr 5026 intirr 5029 dffun3 5120 dffun4 5121 dffun5 5122 dffun6f 5123 dffun7 5133 funopab 5139 funcnv2 5155 funcnv 5156 fun11 5159 fununi 5160 funcnvuni 5161 fnres 5199 fnopabg 5205 dff13 5471 fvfullfunlem1 5861 clos1induct 5880 dfnnc3 5885 frds 5935 enmap2lem4 6066 enmap1lem4 6072 ncssfin 6151 spacind 6287 |
Copyright terms: Public domain | W3C validator |