![]() |
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 3073 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) | |
2 | 1 | con2bii 357 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∀wral 3062 ∃wrex 3071 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-ral 3063 df-rex 3072 |
This theorem is referenced by: rexanali 3103 rexbiOLD 3106 r19.23v 3177 nfrexdw 3291 cbvrexf 3332 nfrexd 3344 rspcimedv 3570 rexab 3650 sbcrext 3827 cbvrexcsf 3899 rabn0 4343 r19.9rzv 4455 rexn0 4466 rexsng 4633 rexxfrd 5362 rexxfr2d 5364 rexxfrd2 5366 rexxfr 5369 rexiunxp 5794 rexxpf 5801 rexrnmptw 7041 rexrnmpt 7043 cbvexfo 7232 rexrnmpo 7489 tz7.49 8383 dfsup2 9338 supnub 9356 infnlb 9386 wofib 9439 zfregs2 9627 alephval3 10004 ac6n 10379 prmreclem5 16746 sylow1lem3 19335 ordtrest2lem 22500 trfil2 23184 alexsubALTlem3 23346 alexsubALTlem4 23347 evth 24268 lhop1lem 25323 nosupbnd1lem4 27005 vdn0conngrumgrv2 28985 nmobndseqi 29566 chpssati 31150 chrelat3 31158 nn0min 31558 xrnarchi 31862 0nellinds 32001 ordtrest2NEWlem 32331 dffr5 34159 poimirlem1 36011 poimirlem26 36036 poimirlem27 36037 fdc 36136 lpssat 37407 lssat 37410 lfl1 37464 atlrelat1 37715 unxpwdom3 41325 onsupeqnmax 41484 sucomisnotcard 41721 ss2iundf 41836 zfregs2VD 43028 |
Copyright terms: Public domain | W3C validator |