Theorem rabid2 3339

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 2913	. . 3 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
2		pm4.71 558	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
3	2	albii 1802	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
4	1, 3	bitr4i 279	. 2 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
5		df-rab 3113	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6	5	eqeq2i 2806	. 2 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)})
7		df-ral 3109	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
8	4, 6, 7	3bitr4i 304	1 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1520   = wceq 1522   ∈ wcel 2080  {cab 2774  ∀wral 3104  {crab 3108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-ext 2768

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-clab 2775  df-cleq 2787  df-clel 2862  df-ral 3109  df-rab 3113

This theorem is referenced by:  rabxm  4262  iinrab2  4893  riinrab  4907  class2seteq  5149  dmmptg  5974  wfisg  6061  dmmptd  6364  fneqeql  6684  fmpt  6740  zfrep6  7515  axdc2lem  9719  ioomax  12661  iccmax  12662  hashbc  13659  lcmf0  15807  dfphi2  15940  phiprmpw  15942  phisum  15956  isnsg4  18076  symggen2  18330  psgnfvalfi  18372  lssuni  19401  psr1baslem  20036  psgnghm2  20407  ocv0  20503  dsmmfi  20564  frlmfibas  20588  frlmlbs  20623  ordtrest2lem  21495  comppfsc  21824  xkouni  21891  xkoccn  21911  tsmsfbas  22419  clsocv  23536  ehlbase  23701  ovolicc2lem4  23804  itg2monolem1  24034  musum  25450  lgsquadlem2  25639  umgr2v2evd2  26992  frgrregorufr0  27787  ubthlem1  28330  xrsclat  30333  psgndmfi  30654  ordtrest2NEWlem  30774  hasheuni  30953  measvuni  31082  imambfm  31129  subfacp1lem6  32034  connpconn  32084  cvmliftmolem2  32131  cvmlift2lem12  32163  tfisg  32658  frpoinsg  32684  frinsg  32690  poimirlem28  34464  fdc  34565  isbnd3  34607  pmap1N  36447  pol1N  36590  dia1N  37733  dihwN  37969  vdioph  38874  fiphp3d  38914  dmmptdf  41041  stirlinglem14  41928  fvmptrabdm  43022  suppdm  44060