Theorem rabid2 3096

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 2719	. . 3 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
2		pm4.71 660	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
3	2	albii 1737	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
4	1, 3	bitr4i 266	. 2 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
5		df-rab 2905	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6	5	eqeq2i 2622	. 2 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)})
7		df-ral 2901	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
8	4, 6, 7	3bitr4i 291	1 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473   = wceq 1475   ∈ wcel 1977  {cab 2596  ∀wral 2896  {crab 2900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-ral 2901  df-rab 2905

This theorem is referenced by:  rabxm  3915  iinrab2  4519  riinrab  4532  class2seteq  4759  dmmptg  5549  wfisg  5632  dmmptd  5937  fneqeql  6233  fmpt  6289  zfrep6  7027  axdc2lem  9153  ioomax  12119  iccmax  12120  hashbc  13094  lcmf0  15185  dfphi2  15317  phiprmpw  15319  phisum  15333  isnsg4  17460  symggen2  17714  psgnfvalfi  17756  lssuni  18761  psr1baslem  19376  psgnghm2  19746  ocv0  19840  dsmmfi  19901  frlmfibas  19924  frlmlbs  19955  ordtrest2lem  20817  comppfsc  21145  xkouni  21212  xkoccn  21232  tsmsfbas  21741  clsocv  22857  ehlbase  23002  ovolicc2lem4  23095  itg2monolem1  23323  musum  24717  lgsquadlem2  24906  vdgr1d  26430  vdgr1b  26431  frgraregorufr0  26579  ubthlem1  27110  xrsclat  29011  psgndmfi  29177  ordtrest2NEWlem  29296  hasheuni  29474  measvuni  29604  imambfm  29651  subfacp1lem6  30421  conpcon  30471  cvmliftmolem2  30518  cvmlift2lem12  30550  tfisg  30960  frinsg  30986  poimirlem28  32607  fdc  32711  isbnd3  32753  pmap1N  34071  pol1N  34214  dia1N  35360  dihwN  35596  vdioph  36361  fiphp3d  36401  dmmptdf  38412  stirlinglem14  38980  umgr2v2evd2  40743  frgrregorufr0  41489  suppdm  42094