![]() |
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 2244 | . 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑥 ∣ 𝜑}) |
3 | abid 2165 | . 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) | |
4 | 2, 3 | bitri 184 | 1 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 = wceq 1353 ∈ wcel 2148 {cab 2163 |
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-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 |
This theorem is referenced by: rabid 2653 vex 2742 csbco 3069 csbcow 3070 csbnestgf 3111 ifmdc 3576 pwss 3593 snsspw 3766 iunpw 4482 ordon 4487 funcnv3 5280 tfrlem4 6316 tfrlem8 6321 tfrlem9 6322 tfrlemibxssdm 6330 tfr1onlembxssdm 6346 tfrcllembxssdm 6359 ixpm 6732 mapsnen 6813 sbthlem1 6958 1idprl 7591 1idpru 7592 recexprlem1ssl 7634 recexprlem1ssu 7635 recexprlemss1l 7636 recexprlemss1u 7637 txbas 13843 |
Copyright terms: Public domain | W3C validator |