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 2732 | . . 3 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))) | |
2 | pm4.71 662 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))) | |
3 | 2 | albii 1747 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))) |
4 | 1, 3 | bitr4i 267 | . 2 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
5 | df-rab 2921 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
6 | 5 | eqeq2i 2634 | . 2 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}) |
7 | df-ral 2917 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
8 | 4, 6, 7 | 3bitr4i 292 | 1 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∀wal 1481 = wceq 1483 ∈ wcel 1990 {cab 2608 ∀wral 2912 {crab 2916 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-ral 2917 df-rab 2921 |
This theorem is referenced by: rabxm 3961 iinrab2 4583 riinrab 4596 class2seteq 4833 dmmptg 5632 wfisg 5715 dmmptd 6024 fneqeql 6325 fmpt 6381 zfrep6 7134 axdc2lem 9270 ioomax 12248 iccmax 12249 hashbc 13237 lcmf0 15347 dfphi2 15479 phiprmpw 15481 phisum 15495 isnsg4 17637 symggen2 17891 psgnfvalfi 17933 lssuni 18940 psr1baslem 19555 psgnghm2 19927 ocv0 20021 dsmmfi 20082 frlmfibas 20105 frlmlbs 20136 ordtrest2lem 21007 comppfsc 21335 xkouni 21402 xkoccn 21422 tsmsfbas 21931 clsocv 23049 ehlbase 23194 ovolicc2lem4 23288 itg2monolem1 23517 musum 24917 lgsquadlem2 25106 umgr2v2evd2 26423 frgrregorufr0 27188 ubthlem1 27726 xrsclat 29680 psgndmfi 29846 ordtrest2NEWlem 29968 hasheuni 30147 measvuni 30277 imambfm 30324 subfacp1lem6 31167 connpconn 31217 cvmliftmolem2 31264 cvmlift2lem12 31296 tfisg 31716 frinsg 31742 poimirlem28 33437 fdc 33541 isbnd3 33583 pmap1N 35053 pol1N 35196 dia1N 36342 dihwN 36578 vdioph 37343 fiphp3d 37383 dmmptdf 39417 stirlinglem14 40304 suppdm 42300 |
Copyright terms: Public domain | W3C validator |