New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > rexnal | Unicode version |
Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) |
Ref | Expression |
---|---|
rexnal |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rex 2620 | . 2 | |
2 | exanali 1585 | . . 3 | |
3 | df-ral 2619 | . . 3 | |
4 | 2, 3 | xchbinxr 302 | . 2 |
5 | 1, 4 | bitri 240 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wb 176 wa 358 wal 1540 wex 1541 wcel 1710 wral 2614 wrex 2615 |
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 df-an 360 df-ex 1542 df-ral 2619 df-rex 2620 |
This theorem is referenced by: dfral2 2626 rexanali 2660 2ralor 2780 uni0b 3916 iundif2 4033 dfint3 4318 dfnnc2 4395 nndisjeq 4429 ncfinraiselem2 4480 nnpweqlem1 4522 rexxpf 4828 transex 5910 refex 5911 antisymex 5912 connexex 5913 extex 5915 symex 5916 nchoicelem11 6299 |
Copyright terms: Public domain | W3C validator |