![]() |
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 3072 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) | |
2 | 1 | con2bii 358 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∀wral 3061 ∃wrex 3070 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-ral 3062 df-rex 3071 |
This theorem is referenced by: rexanali 3102 rexbiOLD 3105 r19.23v 3176 nfrexdw 3292 cbvrexf 3333 nfrexd 3345 rspcimedv 3571 rexab 3653 sbcrext 3830 cbvrexcsf 3902 rabn0 4346 r19.9rzv 4458 rexn0 4469 rexsng 4636 rexxfrd 5365 rexxfr2d 5367 rexxfrd2 5369 rexxfr 5372 rexiunxp 5797 rexxpf 5804 rexrnmptw 7046 rexrnmpt 7048 cbvexfo 7237 rexrnmpo 7496 tz7.49 8392 dfsup2 9385 supnub 9403 infnlb 9433 wofib 9486 zfregs2 9674 alephval3 10051 ac6n 10426 prmreclem5 16797 sylow1lem3 19387 ordtrest2lem 22570 trfil2 23254 alexsubALTlem3 23416 alexsubALTlem4 23417 evth 24338 lhop1lem 25393 nosupbnd1lem4 27075 vdn0conngrumgrv2 29182 nmobndseqi 29763 chpssati 31347 chrelat3 31355 nn0min 31765 xrnarchi 32069 0nellinds 32206 ordtrest2NEWlem 32560 dffr5 34383 poimirlem1 36125 poimirlem26 36150 poimirlem27 36151 fdc 36250 lpssat 37521 lssat 37524 lfl1 37578 atlrelat1 37829 unxpwdom3 41465 onsupeqnmax 41624 sucomisnotcard 41904 ss2iundf 42019 zfregs2VD 43211 |
Copyright terms: Public domain | W3C validator |