Theorem rabid2 3381

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 2945	. . 3 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
2		pm4.71 560	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
3	2	albii 1820	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
4	1, 3	bitr4i 280	. 2 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
5		df-rab 3147	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6	5	eqeq2i 2834	. 2 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)})
7		df-ral 3143	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
8	4, 6, 7	3bitr4i 305	1 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1535   = wceq 1537   ∈ wcel 2114  {cab 2799  ∀wral 3138  {crab 3142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-ral 3143  df-rab 3147

This theorem is referenced by:  rabxm  4340  iinrab2  4992  riinrab  5006  class2seteq  5255  dmmptg  6096  wfisg  6183  dmmptd  6493  fneqeql  6816  fmpt  6874  zfrep6  7656  axdc2lem  9870  ioomax  12812  iccmax  12813  hashbc  13812  lcmf0  15978  dfphi2  16111  phiprmpw  16113  phisum  16127  isnsg4  18319  symggen2  18599  psgnfvalfi  18641  lssuni  19711  psr1baslem  20353  psgnghm2  20725  ocv0  20821  dsmmfi  20882  frlmfibas  20906  frlmlbs  20941  ordtrest2lem  21811  comppfsc  22140  xkouni  22207  xkoccn  22227  tsmsfbas  22736  clsocv  23853  ehlbase  24018  ovolicc2lem4  24121  itg2monolem1  24351  musum  25768  lgsquadlem2  25957  umgr2v2evd2  27309  frgrregorufr0  28103  ubthlem1  28647  xrsclat  30667  psgndmfi  30740  ordtrest2NEWlem  31165  hasheuni  31344  measvuni  31473  imambfm  31520  subfacp1lem6  32432  connpconn  32482  cvmliftmolem2  32529  cvmlift2lem12  32561  tfisg  33055  frpoinsg  33081  frinsg  33087  poimirlem28  34935  fdc  35035  isbnd3  35077  pmap1N  36918  pol1N  37061  dia1N  38204  dihwN  38440  vdioph  39396  fiphp3d  39436  dmmptdf  41508  stirlinglem14  42392  fvmptrabdm  43512  suppdm  44585