Theorem rabid2 3283

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 561	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
3	2	albii 1827	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
4	1, 3	bitr4i 281	. 2 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
5		df-rab 3060	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6	5	eqeq2i 2749	. 2 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)})
7		df-ral 3056	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
8	4, 6, 7	3bitr4i 306	1 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1541   = wceq 1543   ∈ wcel 2112  {cab 2714  ∀wral 3051  {crab 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-rab 3060

This theorem is referenced by:  rabxm  4287  iinrab2  4964  riinrab  4978  class2seteq  5231  dmmptg  6085  frpoinsg  6175  wfisg  6183  dmmptd  6501  fneqeql  6844  fmpt  6905  zfrep6  7706  axdc2lem  10027  ioomax  12975  iccmax  12976  hashbc  13982  lcmf0  16154  dfphi2  16290  phiprmpw  16292  phisum  16306  isnsg4  18537  symggen2  18817  psgnfvalfi  18859  lssuni  19930  psgnghm2  20497  ocv0  20593  dsmmfi  20654  frlmfibas  20678  frlmlbs  20713  psr1baslem  21060  ordtrest2lem  22054  comppfsc  22383  xkouni  22450  xkoccn  22470  tsmsfbas  22979  clsocv  24101  ehlbase  24266  ovolicc2lem4  24371  itg2monolem1  24602  musum  26027  lgsquadlem2  26216  umgr2v2evd2  27569  frgrregorufr0  28361  ubthlem1  28905  xrsclat  30962  psgndmfi  31038  zarcls0  31486  ordtrest2NEWlem  31540  hasheuni  31719  measvuni  31848  imambfm  31895  subfacp1lem6  32814  connpconn  32864  cvmliftmolem2  32911  cvmlift2lem12  32943  tfisg  33456  frinsg  33462  poimirlem28  35491  fdc  35589  isbnd3  35628  pmap1N  37467  pol1N  37610  dia1N  38753  dihwN  38989  vdioph  40245  fiphp3d  40285  dmmptdf  42377  stirlinglem14  43246  fvmptrabdm  44400  suppdm  45467