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 3233 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) | |
2 | 1 | con2bii 359 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 207 ∀wral 3135 ∃wrex 3136 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-ral 3140 df-rex 3141 |
This theorem is referenced by: rexim 3238 rexanali 3262 r19.23v 3276 nfrexd 3304 nfrexdg 3305 r19.30OLD 3336 cbvrexfw 3436 cbvrexf 3438 rspcimedv 3611 sbcrext 3853 cbvrexcsf 3923 rabn0 4336 r19.9rzv 4441 rexxfrd 5300 rexxfr2d 5302 rexxfrd2 5304 rexxfr 5307 rexiunxp 5704 rexxpf 5711 rexrnmptw 6853 rexrnmpt 6855 cbvexfo 7037 rexrnmpo 7279 tz7.49 8070 dfsup2 8896 supnub 8914 infnlb 8944 wofib 8997 zfregs2 9163 alephval3 9524 ac6n 9895 prmreclem5 16244 sylow1lem3 18654 ordtrest2lem 21739 trfil2 22423 alexsubALTlem3 22585 alexsubALTlem4 22586 evth 23490 lhop1lem 24537 vdn0conngrumgrv2 27902 nmobndseqi 28483 chpssati 30067 chrelat3 30075 nn0min 30463 xrnarchi 30740 0nellinds 30862 ordtrest2NEWlem 31064 dffr5 32886 nosupbnd1lem4 33108 poimirlem1 34774 poimirlem26 34799 poimirlem27 34800 fdc 34901 lpssat 36029 lssat 36032 lfl1 36086 atlrelat1 36337 unxpwdom3 39573 ss2iundf 39882 zfregs2VD 41052 |
Copyright terms: Public domain | W3C validator |