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 3235. (Revised by Wolf Lammen, 9-Dec-2019.) |
Ref | Expression |
---|---|
dfral2 | ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notnotb 316 | . . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑) | |
2 | 1 | ralbii 3162 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ¬ ¬ 𝜑) |
3 | ralnex 3233 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑) | |
4 | 2, 3 | bitri 276 | 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: rexnal 3235 boxcutc 8493 infssuni 8803 ac6n 9895 indstr 12304 trfil3 22424 tglowdim2ln 26364 nmobndseqi 28483 stri 29961 hstri 29969 reprinfz1 31792 bnj1204 32181 nosepon 33069 fvineqsneq 34575 poimirlem1 34774 n0elqs 35464 |
Copyright terms: Public domain | W3C validator |