![]() |
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 1451 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦)) | |
2 | ax-14 1451 | . . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥)) | |
3 | 2 | equcoms 1642 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥)) |
4 | 1, 3 | impbid 128 | 1 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 |
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-gen 1384 ax-ie2 1429 ax-8 1441 ax-14 1451 ax-17 1465 ax-i9 1469 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: elsb4 1902 dveel2 1946 axext3 2072 axext4 2073 bm1.1 2074 eleq2w 2150 bm1.3ii 3966 nalset 3975 zfun 4270 fv3 5341 tfrlemisucaccv 6104 tfr1onlemsucaccv 6120 tfrcllemsucaccv 6133 bdsepnft 12044 bdsepnfALT 12046 bdbm1.3ii 12048 bj-nalset 12052 bj-nnelirr 12114 strcollnft 12145 strcollnfALT 12147 nninfalllem1 12165 nninfsellemeq 12172 nninfsellemqall 12173 nninfsellemeqinf 12174 nninfomni 12177 |
Copyright terms: Public domain | W3C validator |