![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > abbi2i | GIF version |
Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
abbiri.1 | ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) |
Ref | Expression |
---|---|
abbi2i | ⊢ 𝐴 = {𝑥 ∣ 𝜑} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abeq2 2203 | . 2 ⊢ (𝐴 = {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝜑)) | |
2 | abbiri.1 | . 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) | |
3 | 1, 2 | mpgbir 1394 | 1 ⊢ 𝐴 = {𝑥 ∣ 𝜑} |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 = wceq 1296 ∈ wcel 1445 {cab 2081 |
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-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-11 1449 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 |
This theorem is referenced by: abid2 2215 cbvralcsf 3004 cbvrexcsf 3005 cbvreucsf 3006 cbvrabcsf 3007 symdifxor 3281 dfnul2 3304 dfpr2 3485 dftp2 3511 0iin 3810 pwpwab 3838 epse 4193 fv3 5363 fo1st 5966 fo2nd 5967 xp2 5981 tfrlem3 6114 tfr1onlem3 6141 mapsn 6487 ixpconstg 6504 ixp0x 6523 nnzrab 8872 nn0zrab 8873 |
Copyright terms: Public domain | W3C validator |