Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dfral2 | Structured version Visualization version GIF version |
Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) Allow shortening of rexnal 3238. (Revised by Wolf Lammen, 9-Dec-2019.) |
Ref | Expression |
---|---|
dfral2 | ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notnotb 317 | . . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑) | |
2 | 1 | ralbii 3165 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ¬ ¬ 𝜑) |
3 | ralnex 3236 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑) | |
4 | 2, 3 | bitri 277 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 208 ∀wral 3138 ∃wrex 3139 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-ral 3143 df-rex 3144 |
This theorem is referenced by: rexnal 3238 boxcutc 8505 infssuni 8815 ac6n 9907 indstr 12317 trfil3 22496 tglowdim2ln 26437 nmobndseqi 28556 stri 30034 hstri 30042 reprinfz1 31893 bnj1204 32284 nosepon 33172 fvineqsneq 34696 poimirlem1 34908 n0elqs 35598 |
Copyright terms: Public domain | W3C validator |