![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dfrex2 | Structured version Visualization version Unicode version |
Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Wolf Lammen, 26-Nov-2019.) |
Ref | Expression |
---|---|
dfrex2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralnex 2833 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | con2bii 334 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 |
This theorem depends on definitions: df-bi 189 df-an 373 df-ex 1663 df-ral 2741 df-rex 2742 |
This theorem is referenced by: rexanali 2839 nfrexd 2848 nfrexOLD 2850 rexim 2851 r19.23v 2866 r19.30 2934 r19.35 2936 cbvrexf 3013 rspcimedv 3151 sbcrext 3340 cbvrexcsf 3395 r19.9rzv 3862 rexxfrd 4614 rexxfr2d 4616 rexxfr 4619 rexiunxp 4974 rexxpf 4981 rexrnmpt 6030 cbvexfo 6186 rexrnmpt2 6409 tz7.49 7159 dfsup2 7955 supnub 7973 infnlb 8005 wofib 8057 zfregs2 8214 alephval3 8538 ac6n 8912 prmreclem5 14857 sylow1lem3 17245 ordtrest2lem 20212 trfil2 20895 alexsubALTlem3 21057 alexsubALTlem4 21058 evth 21980 lhop1lem 22958 nmobndseqi 26413 chpssati 28009 chrelat3 28017 nn0min 28377 xrnarchi 28494 ordtrest2NEWlem 28721 dffr5 30386 poimirlem1 31934 poimirlem26 31959 poimirlem27 31960 fdc 32067 lpssat 32573 lssat 32576 lfl1 32630 atlrelat1 32881 unxpwdom3 35947 ss2iundf 36245 zfregs2VD 37231 rexxfrd2 39003 |
Copyright terms: Public domain | W3C validator |