Theorem rabid2 3249

Description: An "identity" law for restricted class abstraction. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)

Assertion

Ref	Expression
rabid2	⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem 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 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)

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