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 2398 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜑)) | |
2 | alinexa 1567 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
3 | df-rex 2399 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
4 | 2, 3 | xchbinxr 657 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝜑) ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) |
5 | 1, 4 | bitri 183 | 1 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 ∀wal 1314 ∃wex 1453 ∈ wcel 1465 ∀wral 2393 ∃wrex 2394 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 588 ax-in2 589 ax-5 1408 ax-gen 1410 ax-ie2 1455 |
This theorem depends on definitions: df-bi 116 df-tru 1319 df-fal 1322 df-ral 2398 df-rex 2399 |
This theorem is referenced by: rexalim 2407 ralinexa 2439 nrex 2501 nrexdv 2502 ralnex2 2548 uni0b 3731 iindif2m 3850 f0rn0 5287 supmoti 6848 fodjuomnilemdc 6984 ismkvnex 6997 suprnubex 8679 icc0r 9677 ioo0 10005 ico0 10007 ioc0 10008 prmind2 11728 sqrt2irr 11767 |
Copyright terms: Public domain | W3C validator |