![]() |
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 2862 | . . 3 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))) | |
2 | pm4.71 665 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))) | |
3 | 2 | albii 1888 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))) |
4 | 1, 3 | bitr4i 267 | . 2 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
5 | df-rab 3051 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
6 | 5 | eqeq2i 2764 | . 2 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}) |
7 | df-ral 3047 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
8 | 4, 6, 7 | 3bitr4i 292 | 1 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 ∀wal 1622 = wceq 1624 ∈ wcel 2131 {cab 2738 ∀wral 3042 {crab 3046 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-clab 2739 df-cleq 2745 df-clel 2748 df-ral 3047 df-rab 3051 |
This theorem is referenced by: rabxm 4096 iinrab2 4727 riinrab 4740 class2seteq 4974 dmmptg 5785 wfisg 5868 dmmptd 6177 fneqeql 6480 fmpt 6536 zfrep6 7291 axdc2lem 9454 ioomax 12433 iccmax 12434 hashbc 13421 lcmf0 15541 dfphi2 15673 phiprmpw 15675 phisum 15689 isnsg4 17830 symggen2 18083 psgnfvalfi 18125 lssuni 19134 psr1baslem 19749 psgnghm2 20121 ocv0 20215 dsmmfi 20276 frlmfibas 20299 frlmlbs 20330 ordtrest2lem 21201 comppfsc 21529 xkouni 21596 xkoccn 21616 tsmsfbas 22124 clsocv 23241 ehlbase 23386 ovolicc2lem4 23480 itg2monolem1 23708 musum 25108 lgsquadlem2 25297 umgr2v2evd2 26625 frgrregorufr0 27470 ubthlem1 28027 xrsclat 29981 psgndmfi 30147 ordtrest2NEWlem 30269 hasheuni 30448 measvuni 30578 imambfm 30625 subfacp1lem6 31466 connpconn 31516 cvmliftmolem2 31563 cvmlift2lem12 31595 tfisg 32013 frpoinsg 32039 frinsg 32043 poimirlem28 33742 fdc 33846 isbnd3 33888 pmap1N 35548 pol1N 35691 dia1N 36836 dihwN 37072 vdioph 37837 fiphp3d 37877 dmmptdf 39908 stirlinglem14 40799 fvmptrabdm 41809 suppdm 42802 |
Copyright terms: Public domain | W3C validator |