Theorem rabid2 3255

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 2868	. . 3 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
2		pm4.71 665	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
3	2	albii 1894	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
4	1, 3	bitr4i 267	. 2 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
5		df-rab 3057	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6	5	eqeq2i 2770	. 2 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)})
7		df-ral 3053	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
8	4, 6, 7	3bitr4i 292	1 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383  ∀wal 1628   = wceq 1630   ∈ wcel 2137  {cab 2744  ∀wral 3048  {crab 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-ral 3053  df-rab 3057

This theorem is referenced by:  rabxm  4102  iinrab2  4733  riinrab  4746  class2seteq  4980  dmmptg  5791  wfisg  5874  dmmptd  6183  fneqeql  6486  fmpt  6542  zfrep6  7297  axdc2lem  9460  ioomax  12439  iccmax  12440  hashbc  13427  lcmf0  15547  dfphi2  15679  phiprmpw  15681  phisum  15695  isnsg4  17836  symggen2  18089  psgnfvalfi  18131  lssuni  19140  psr1baslem  19755  psgnghm2  20127  ocv0  20221  dsmmfi  20282  frlmfibas  20305  frlmlbs  20336  ordtrest2lem  21207  comppfsc  21535  xkouni  21602  xkoccn  21622  tsmsfbas  22130  clsocv  23247  ehlbase  23392  ovolicc2lem4  23486  itg2monolem1  23714  musum  25114  lgsquadlem2  25303  umgr2v2evd2  26631  frgrregorufr0  27476  ubthlem1  28033  xrsclat  29987  psgndmfi  30153  ordtrest2NEWlem  30275  hasheuni  30454  measvuni  30584  imambfm  30631  subfacp1lem6  31472  connpconn  31522  cvmliftmolem2  31569  cvmlift2lem12  31601  tfisg  32019  frpoinsg  32045  frinsg  32049  poimirlem28  33748  fdc  33852  isbnd3  33894  pmap1N  35554  pol1N  35697  dia1N  36842  dihwN  37078  vdioph  37843  fiphp3d  37883  dmmptdf  39914  stirlinglem14  40805  fvmptrabdm  41815  suppdm  42808