| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Relationship between restricted universal and existential quantifiers. |
| Ref | Expression |
|---|---|
| ralnex |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | alinexa 1083 |
. 2
| |
| 2 | df-ral 1696 |
. 2
| |
| 3 | df-rex 1697 |
. . 3
| |
| 4 | 3 | notbii 194 |
. 2
|
| 5 | 1, 2, 4 | 3bitr4i 190 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: dfrex2 1703 ralinexa 1730 nrex 1776 nrexdv 1777 ra4esbca 2049 iindif2 2666 ordunisuc2 3172 tfi 3183 rexxp 3276 canth 3965 omsdomnn 4594 isfinite2 4609 supmo 4636 elirrv 4658 unbndrank 4745 ac9s 4826 kmlem7 4833 kmlem8 4834 kmlem13 4839 zorn2lem4 4853 arch 6153 xrsupsslem 6158 xrinfmsslem 6159 supxrre 6165 supxrbnd 6173 supxrbnd1 6177 supxrbnd2 6178 sqr2irrlem3 6816 climunii 7188 clsval2 7770 ntreq0 7793 qdensere 7836 bcthlem7 8090 bcthlem28 8111 nmounbi 8523 lnon0 8542 hlimuniii 9191 largei 10278 cvbr2 10294 chrelat2i 10376 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-gen 1004 ax-4 1014 ax-5o 1016 |
| This theorem depends on definitions: df-bi 154 df-an 232 df-ex 1022 df-ral 1696 df-rex 1697 |