Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rabid2 | Structured version Visualization version 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 2945 | . . 3 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))) | |
2 | pm4.71 558 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))) | |
3 | 2 | albii 1811 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))) |
4 | 1, 3 | bitr4i 279 | . 2 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
5 | df-rab 3147 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
6 | 5 | eqeq2i 2834 | . 2 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}) |
7 | df-ral 3143 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
8 | 4, 6, 7 | 3bitr4i 304 | 1 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∀wal 1526 = wceq 1528 ∈ wcel 2105 {cab 2799 ∀wral 3138 {crab 3142 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-ral 3143 df-rab 3147 |
This theorem is referenced by: rabxm 4339 iinrab2 4984 riinrab 4998 class2seteq 5247 dmmptg 6090 wfisg 6177 dmmptd 6487 fneqeql 6809 fmpt 6867 zfrep6 7647 axdc2lem 9859 ioomax 12801 iccmax 12802 hashbc 13801 lcmf0 15968 dfphi2 16101 phiprmpw 16103 phisum 16117 isnsg4 18259 symggen2 18530 psgnfvalfi 18572 lssuni 19642 psr1baslem 20283 psgnghm2 20655 ocv0 20751 dsmmfi 20812 frlmfibas 20836 frlmlbs 20871 ordtrest2lem 21741 comppfsc 22070 xkouni 22137 xkoccn 22157 tsmsfbas 22665 clsocv 23782 ehlbase 23947 ovolicc2lem4 24050 itg2monolem1 24280 musum 25696 lgsquadlem2 25885 umgr2v2evd2 27237 frgrregorufr0 28031 ubthlem1 28575 xrsclat 30595 psgndmfi 30668 ordtrest2NEWlem 31065 hasheuni 31244 measvuni 31373 imambfm 31420 subfacp1lem6 32330 connpconn 32380 cvmliftmolem2 32427 cvmlift2lem12 32459 tfisg 32953 frpoinsg 32979 frinsg 32985 poimirlem28 34802 fdc 34903 isbnd3 34945 pmap1N 36785 pol1N 36928 dia1N 38071 dihwN 38307 vdioph 39256 fiphp3d 39296 dmmptdf 41368 stirlinglem14 42253 fvmptrabdm 43373 suppdm 44463 |
Copyright terms: Public domain | W3C validator |