| 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 3100. (Revised by Wolf Lammen, 9-Dec-2019.) |
| Ref | Expression |
|---|---|
| dfral2 | ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | notnotb 315 | . . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑) | |
| 2 | 1 | ralbii 3093 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ¬ ¬ 𝜑) |
| 3 | ralnex 3072 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑) | |
| 4 | 2, 3 | bitri 275 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ↔ wb 206 ∀wral 3061 ∃wrex 3070 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-ral 3062 df-rex 3071 |
| This theorem is referenced by: rexnal 3100 imaeqsalvOLD 7384 boxcutc 8981 infssuni 9386 ac6n 10525 indstr 12958 trfil3 23896 nosepon 27710 noinfbnd1lem4 27771 cuteq1 27878 tglowdim2ln 28659 nmobndseqi 30798 stri 32276 hstri 32284 reprinfz1 34637 bnj1204 35026 fvineqsneq 37413 poimirlem1 37628 n0elqs 38327 |
| Copyright terms: Public domain | W3C validator |