Theorem rabid2 3107

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 2729	. . 3 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
2		pm4.71 661	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
3	2	albii 1744	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
4	1, 3	bitr4i 267	. 2 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
5		df-rab 2916	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6	5	eqeq2i 2633	. 2 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)})
7		df-ral 2912	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
8	4, 6, 7	3bitr4i 292	1 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384  ∀wal 1478   = wceq 1480   ∈ wcel 1987  {cab 2607  ∀wral 2907  {crab 2911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-ral 2912  df-rab 2916

This theorem is referenced by:  rabxm  3935  iinrab2  4549  riinrab  4562  class2seteq  4793  dmmptg  5591  wfisg  5674  dmmptd  5981  fneqeql  6281  fmpt  6337  zfrep6  7081  axdc2lem  9214  ioomax  12190  iccmax  12191  hashbc  13175  lcmf0  15271  dfphi2  15403  phiprmpw  15405  phisum  15419  isnsg4  17558  symggen2  17812  psgnfvalfi  17854  lssuni  18859  psr1baslem  19474  psgnghm2  19846  ocv0  19940  dsmmfi  20001  frlmfibas  20024  frlmlbs  20055  ordtrest2lem  20917  comppfsc  21245  xkouni  21312  xkoccn  21332  tsmsfbas  21841  clsocv  22957  ehlbase  23102  ovolicc2lem4  23195  itg2monolem1  23423  musum  24817  lgsquadlem2  25006  umgr2v2evd2  26309  frgrregorufr0  27047  ubthlem1  27572  xrsclat  29462  psgndmfi  29628  ordtrest2NEWlem  29747  hasheuni  29925  measvuni  30055  imambfm  30102  subfacp1lem6  30872  connpconn  30922  cvmliftmolem2  30969  cvmlift2lem12  31001  tfisg  31414  frinsg  31440  poimirlem28  33066  fdc  33170  isbnd3  33212  pmap1N  34530  pol1N  34673  dia1N  35819  dihwN  36055  vdioph  36820  fiphp3d  36860  dmmptdf  38888  stirlinglem14  39608  suppdm  41585