Theorem rabid2 3383

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

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

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 2795

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 2802  df-cleq 2816  df-clel 2895  df-ral 3145  df-rab 3149

This theorem is referenced by:  rabxm  4342  iinrab2  4994  riinrab  5008  class2seteq  5257  dmmptg  6098  wfisg  6185  dmmptd  6495  fneqeql  6818  fmpt  6876  zfrep6  7658  axdc2lem  9872  ioomax  12814  iccmax  12815  hashbc  13814  lcmf0  15980  dfphi2  16113  phiprmpw  16115  phisum  16129  isnsg4  18321  symggen2  18601  psgnfvalfi  18643  lssuni  19713  psr1baslem  20355  psgnghm2  20727  ocv0  20823  dsmmfi  20884  frlmfibas  20908  frlmlbs  20943  ordtrest2lem  21813  comppfsc  22142  xkouni  22209  xkoccn  22229  tsmsfbas  22738  clsocv  23855  ehlbase  24020  ovolicc2lem4  24123  itg2monolem1  24353  musum  25770  lgsquadlem2  25959  umgr2v2evd2  27311  frgrregorufr0  28105  ubthlem1  28649  xrsclat  30669  psgndmfi  30742  ordtrest2NEWlem  31167  hasheuni  31346  measvuni  31475  imambfm  31522  subfacp1lem6  32434  connpconn  32484  cvmliftmolem2  32531  cvmlift2lem12  32563  tfisg  33057  frpoinsg  33083  frinsg  33089  poimirlem28  34922  fdc  35022  isbnd3  35064  pmap1N  36905  pol1N  37048  dia1N  38191  dihwN  38427  vdioph  39383  fiphp3d  39423  dmmptdf  41495  stirlinglem14  42379  fvmptrabdm  43499  suppdm  44572