![]() |
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.) (Proof shortened by Wolf Lammen, 24-Nov-2024.) |
Ref | Expression |
---|---|
rabid2 | ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2904 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | 1 | rabid2f 3464 | 1 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1542 ∀wral 3062 {crab 3433 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3063 df-rab 3434 |
This theorem is referenced by: class2seteq 3699 rabxm 4385 iinrab2 5072 riinrab 5086 dmmptg 6238 frpoinsg 6341 wfisgOLD 6352 dmmptd 6692 fneqeql 7043 fmpt 7105 tfisg 7838 zfrep6 7936 frinsg 9742 axdc2lem 10439 ioomax 13395 iccmax 13396 hashbc 14408 lcmf0 16567 dfphi2 16703 phiprmpw 16705 phisum 16719 isnsg4 19041 symggen2 19332 psgnfvalfi 19374 lssuni 20538 psgnghm2 21118 ocv0 21214 dsmmfi 21277 frlmfibas 21301 frlmlbs 21336 psr1baslem 21691 ordtrest2lem 22689 comppfsc 23018 xkouni 23085 xkoccn 23105 tsmsfbas 23614 clsocv 24749 ehlbase 24914 ovolicc2lem4 25019 itg2monolem1 25250 musum 26675 lgsquadlem2 26864 umgr2v2evd2 28764 frgrregorufr0 29557 ubthlem1 30101 xrsclat 32159 psgndmfi 32235 primefldgen1 32380 zarcls0 32786 ordtrest2NEWlem 32840 hasheuni 33021 measvuni 33150 imambfm 33199 subfacp1lem6 34114 connpconn 34164 cvmliftmolem2 34211 cvmlift2lem12 34243 poimirlem28 36454 fdc 36551 isbnd3 36590 pmap1N 38576 pol1N 38719 dia1N 39862 dihwN 40098 vdioph 41450 fiphp3d 41490 stirlinglem14 44738 fvmptrabdm 45936 suppdm 47093 |
Copyright terms: Public domain | W3C validator |