![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rabid2 | GIF version |
Description: An "identity" law for restricted class abstraction. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
Ref | Expression |
---|---|
rabid2 | ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abeq2 2208 | . . 3 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))) | |
2 | pm4.71 384 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))) | |
3 | 2 | albii 1414 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))) |
4 | 1, 3 | bitr4i 186 | . 2 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
5 | df-rab 2384 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
6 | 5 | eqeq2i 2110 | . 2 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}) |
7 | df-ral 2380 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
8 | 4, 6, 7 | 3bitr4i 211 | 1 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∀wal 1297 = wceq 1299 ∈ wcel 1448 {cab 2086 ∀wral 2375 {crab 2379 |
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 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-11 1452 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-ral 2380 df-rab 2384 |
This theorem is referenced by: rabxmdc 3341 rabrsndc 3538 class2seteq 4027 dmmptg 4972 dmmptd 5189 fneqeql 5460 fmpt 5502 acexmidlemph 5699 inffiexmid 6729 ssfirab 6750 ioomax 9572 iccmax 9573 dfphi2 11688 phiprmpw 11690 unennn 11702 znnen 11703 |
Copyright terms: Public domain | W3C validator |