Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dfrex2 | Structured version Visualization version GIF 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 3158 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) | |
2 | 1 | con2bii 361 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 209 ∀wral 3061 ∃wrex 3062 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-ral 3066 df-rex 3067 |
This theorem is referenced by: rexim 3163 rexbi 3164 rexanali 3184 r19.23v 3198 nfrexd 3226 nfrexdg 3227 cbvrexfw 3346 cbvrexf 3348 rspcimedv 3528 sbcrext 3785 cbvrexcsf 3857 rabn0 4300 r19.9rzv 4411 rexn0 4422 rexsng 4590 rexxfrd 5302 rexxfr2d 5304 rexxfrd2 5306 rexxfr 5309 rexiunxp 5709 rexxpf 5716 rexrnmptw 6914 rexrnmpt 6916 cbvexfo 7100 rexrnmpo 7349 tz7.49 8181 dfsup2 9060 supnub 9078 infnlb 9108 wofib 9161 zfregs2 9349 alephval3 9724 ac6n 10099 prmreclem5 16473 sylow1lem3 18989 ordtrest2lem 22100 trfil2 22784 alexsubALTlem3 22946 alexsubALTlem4 22947 evth 23856 lhop1lem 24910 vdn0conngrumgrv2 28279 nmobndseqi 28860 chpssati 30444 chrelat3 30452 nn0min 30854 xrnarchi 31157 0nellinds 31280 ordtrest2NEWlem 31586 dffr5 33439 nosupbnd1lem4 33651 poimirlem1 35515 poimirlem26 35540 poimirlem27 35541 fdc 35640 lpssat 36764 lssat 36767 lfl1 36821 atlrelat1 37072 unxpwdom3 40623 ss2iundf 40944 zfregs2VD 42134 |
Copyright terms: Public domain | W3C validator |