![]() |
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 3101. (Revised by Wolf Lammen, 9-Dec-2019.) |
Ref | Expression |
---|---|
dfral2 | ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notnotb 315 | . . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑) | |
2 | 1 | ralbii 3094 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ¬ ¬ 𝜑) |
3 | ralnex 3073 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑) | |
4 | 2, 3 | bitri 275 | 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 1798 ax-4 1812 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-ral 3063 df-rex 3072 |
This theorem is referenced by: rexnal 3101 imaeqsalv 7361 boxcutc 8935 infssuni 9343 ac6n 10480 indstr 12900 trfil3 23392 nosepon 27168 noinfbnd1lem4 27229 cuteq1 27334 tglowdim2ln 27902 nmobndseqi 30032 stri 31510 hstri 31518 reprinfz1 33634 bnj1204 34023 fvineqsneq 36293 poimirlem1 36489 n0elqs 37195 |
Copyright terms: Public domain | W3C validator |