Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > abeq2i | GIF version |
Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996.) |
Ref | Expression |
---|---|
abeqi.1 | ⊢ 𝐴 = {𝑥 ∣ 𝜑} |
Ref | Expression |
---|---|
abeq2i | ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abeqi.1 | . . 3 ⊢ 𝐴 = {𝑥 ∣ 𝜑} | |
2 | 1 | eleq2i 2224 | . 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑥 ∣ 𝜑}) |
3 | abid 2145 | . 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) | |
4 | 2, 3 | bitri 183 | 1 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 = wceq 1335 ∈ wcel 2128 {cab 2143 |
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-5 1427 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-sb 1743 df-clab 2144 df-cleq 2150 df-clel 2153 |
This theorem is referenced by: rabid 2632 vex 2715 csbco 3041 csbcow 3042 csbnestgf 3083 ifmdc 3542 pwss 3559 snsspw 3727 iunpw 4440 ordon 4445 funcnv3 5232 tfrlem4 6260 tfrlem8 6265 tfrlem9 6266 tfrlemibxssdm 6274 tfr1onlembxssdm 6290 tfrcllembxssdm 6303 ixpm 6675 mapsnen 6756 sbthlem1 6901 1idprl 7510 1idpru 7511 recexprlem1ssl 7553 recexprlem1ssu 7554 recexprlemss1l 7555 recexprlemss1u 7556 txbas 12658 |
Copyright terms: Public domain | W3C validator |