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 1477 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦)) | |
2 | ax-14 1477 | . . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥)) | |
3 | 2 | equcoms 1669 | . 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-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-gen 1410 ax-ie2 1455 ax-8 1467 ax-14 1477 ax-17 1491 ax-i9 1495 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: elsb4 1930 dveel2 1974 axext3 2100 axext4 2101 bm1.1 2102 eleq2w 2179 bm1.3ii 4019 nalset 4028 zfun 4326 fv3 5412 tfrlemisucaccv 6190 tfr1onlemsucaccv 6206 tfrcllemsucaccv 6219 acfun 7031 ccfunen 7047 bdsepnft 13012 bdsepnfALT 13014 bdbm1.3ii 13016 bj-nalset 13020 bj-nnelirr 13078 strcollnft 13109 strcollnfALT 13111 nninfalllem1 13130 nninfsellemeq 13137 nninfsellemqall 13138 nninfsellemeqinf 13139 nninfomni 13142 |
Copyright terms: Public domain | W3C validator |