Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ralnex | Unicode version |
Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) |
Ref | Expression |
---|---|
ralnex |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ral 2447 | . 2 | |
2 | alinexa 1590 | . . 3 | |
3 | df-rex 2448 | . . 3 | |
4 | 2, 3 | xchbinxr 673 | . 2 |
5 | 1, 4 | bitri 183 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wa 103 wb 104 wal 1340 wex 1479 wcel 2135 wral 2442 wrex 2443 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-5 1434 ax-gen 1436 ax-ie2 1481 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-fal 1348 df-ral 2447 df-rex 2448 |
This theorem is referenced by: nnral 2454 rexalim 2457 ralinexa 2491 nrex 2556 nrexdv 2557 ralnex2 2603 r19.30dc 2611 uni0b 3808 iindif2m 3927 f0rn0 5376 supmoti 6949 fodjuomnilemdc 7099 ismkvnex 7110 suprnubex 8839 icc0r 9853 ioo0 10185 ico0 10187 ioc0 10188 prmind2 12031 sqrt2irr 12073 nconstwlpolem 13784 |
Copyright terms: Public domain | W3C validator |