Theorem rabid2 3468

Description: An "identity" law for restricted class abstraction. Prefer rabid2im 3467 if one direction is sufficient. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2024.)

Assertion

Ref	Expression
rabid2	⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rabid2

Step	Hyp	Ref	Expression
1		nfcv 2903	. 2 ⊢ Ⅎ𝑥𝐴
2	1	rabid2f 3466	1 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 206   = wceq 1537  ∀wral 3059  {crab 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rab 3434

This theorem is referenced by:  iinrab2  5075  riinrab  5089  dmmptg  6264  frpoinsg  6366  wfisgOLD  6377  dmmptd  6714  fneqeql  7066  fmpt  7130  tfisg  7875  zfrep6  7978  frinsg  9789  axdc2lem  10486  ioomax  13459  iccmax  13460  hashbc  14489  lcmf0  16668  dfphi2  16808  phiprmpw  16810  phisum  16824  isnsg4  19198  symggen2  19504  psgnfvalfi  19546  lssuni  20955  psgnghm2  21617  ocv0  21713  dsmmfi  21776  frlmfibas  21800  frlmlbs  21835  psr1baslem  22202  ordtrest2lem  23227  comppfsc  23556  xkouni  23623  xkoccn  23643  tsmsfbas  24152  clsocv  25298  ehlbase  25463  ovolicc2lem4  25569  itg2monolem1  25800  musum  27249  lgsquadlem2  27440  umgr2v2evd2  29560  frgrregorufr0  30353  ubthlem1  30899  xrsclat  32996  psgndmfi  33101  primefldgen1  33303  zarcls0  33829  ordtrest2NEWlem  33883  hasheuni  34066  measvuni  34195  imambfm  34244  subfacp1lem6  35170  connpconn  35220  cvmliftmolem2  35267  cvmlift2lem12  35299  poimirlem28  37635  fdc  37732  isbnd3  37771  pmap1N  39750  pol1N  39893  dia1N  41036  dihwN  41272  vdioph  42767  fiphp3d  42807  stirlinglem14  46043  fvmptrabdm  47243  suppdm  48356