Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rabid2 | Unicode 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 2273 | . . 3 | |
2 | pm4.71 387 | . . . 4 | |
3 | 2 | albii 1457 | . . 3 |
4 | 1, 3 | bitr4i 186 | . 2 |
5 | df-rab 2451 | . . 3 | |
6 | 5 | eqeq2i 2175 | . 2 |
7 | df-ral 2447 | . 2 | |
8 | 4, 6, 7 | 3bitr4i 211 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 wal 1340 wceq 1342 wcel 2135 cab 2150 wral 2442 crab 2446 |
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 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-11 1493 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-ral 2447 df-rab 2451 |
This theorem is referenced by: rabxmdc 3436 rabrsndc 3639 class2seteq 4137 dmmptg 5096 dmmptd 5313 fneqeql 5588 fmpt 5630 acexmidlemph 5830 inffiexmid 6864 ssfirab 6891 exmidaclem 7156 ioomax 9876 iccmax 9877 dfphi2 12141 phiprmpw 12143 phisum 12161 unennn 12293 znnen 12294 |
Copyright terms: Public domain | W3C validator |