![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ralnex | GIF version |
Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) |
Ref | Expression |
---|---|
ralnex | ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ral 2395 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜑)) | |
2 | alinexa 1565 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
3 | df-rex 2396 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
4 | 2, 3 | xchbinxr 655 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) |
5 | 1, 4 | bitri 183 | 1 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 ∀wal 1312 ∃wex 1451 ∈ wcel 1463 ∀wral 2390 ∃wrex 2391 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 586 ax-in2 587 ax-5 1406 ax-gen 1408 ax-ie2 1453 |
This theorem depends on definitions: df-bi 116 df-tru 1317 df-fal 1320 df-ral 2395 df-rex 2396 |
This theorem is referenced by: rexalim 2404 ralinexa 2436 nrex 2498 nrexdv 2499 ralnex2 2545 uni0b 3727 iindif2m 3846 f0rn0 5275 supmoti 6832 fodjuomnilemdc 6966 ismkvnex 6979 suprnubex 8621 icc0r 9602 ioo0 9930 ico0 9932 ioc0 9933 prmind2 11647 sqrt2irr 11686 |
Copyright terms: Public domain | W3C validator |