![]() |
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 2477 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜑)) | |
2 | alinexa 1614 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
3 | df-rex 2478 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
4 | 2, 3 | xchbinxr 684 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) |
5 | 1, 4 | bitri 184 | 1 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∀wal 1362 ∃wex 1503 ∈ wcel 2164 ∀wral 2472 ∃wrex 2473 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-5 1458 ax-gen 1460 ax-ie2 1505 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-fal 1370 df-ral 2477 df-rex 2478 |
This theorem is referenced by: nnral 2484 rexalim 2487 ralinexa 2521 nrex 2586 nrexdv 2587 ralnex2 2633 r19.30dc 2641 uni0b 3860 iindif2m 3980 f0rn0 5440 supmoti 7042 fodjuomnilemdc 7193 ismkvnex 7204 nninfwlpoimlemginf 7225 suprnubex 8962 icc0r 9982 ioo0 10318 ico0 10320 ioc0 10321 prmind2 12248 sqrt2irr 12290 nconstwlpolem 15500 |
Copyright terms: Public domain | W3C validator |