![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elequ2 | GIF version |
Description: An identity law for the non-logical predicate. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
elequ2 | ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-14 2151 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦)) | |
2 | ax-14 2151 | . . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥)) | |
3 | 2 | equcoms 1708 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥)) |
4 | 1, 3 | impbid 129 | 1 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 |
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-gen 1449 ax-ie2 1494 ax-8 1504 ax-17 1526 ax-i9 1530 ax-14 2151 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: elsb2 2156 dveel2 2158 axext3 2160 axext4 2161 bm1.1 2162 eleq2w 2239 bm1.3ii 4126 nalset 4135 zfun 4436 fv3 5540 tfrlemisucaccv 6329 tfr1onlemsucaccv 6345 tfrcllemsucaccv 6358 acfun 7209 ccfunen 7266 cc1 7267 bdsepnft 14827 bdsepnfALT 14829 bdbm1.3ii 14831 bj-nalset 14835 bj-nnelirr 14893 nninfalllem1 14946 nninfsellemeq 14952 nninfsellemqall 14953 nninfsellemeqinf 14954 nninfomni 14957 |
Copyright terms: Public domain | W3C validator |