Theorem rabid2 3449

Description: An "identity" law for restricted class abstraction. Prefer rabid2im 3448 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 2925	. 2 ⊢ Ⅎ𝑥𝐴
2	1	rabid2f 3447	1 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 209   = wceq 1570  ∀wral 3079  {crab 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rab 3417

This theorem is referenced by:  iinrab2  5034  riinrab  5050  dmmptg  6243  frpoinsg  6344  dmmptd  6680  fneqeql  7041  fmpt  7105  tfisg  7846  zfrep6OLD  7948  frinsg  9719  axdc2lem  10427  ioomax  13444  iccmax  13445  hashbc  14486  lcmf0  16687  dfphi2  16828  phiprmpw  16830  phisum  16845  isnsg4  19228  symggen2  19536  psgnfvalfi  19578  lssuni  21060  psgnghm2  21731  ocv0  21827  dsmmfi  21888  frlmfibas  21912  frlmlbs  21947  psr1baslem  22345  ordtrest2lem  23360  comppfsc  23689  xkouni  23756  xkoccn  23776  tsmsfbas  24285  clsocv  25409  ehlbase  25574  ovolicc2lem4  25679  itg2monolem1  25909  musum  27355  lgsquadlem2  27545  umgr2v2evd2  29877  frgrregorufr0  30675  ubthlem1  31222  xrsclat  33331  psgndmfi  33418  primefldgen1  33642  zarcls0  34258  ordtrest2NEWlem  34312  hasheuni  34475  measvuni  34604  imambfm  34652  subfacp1lem6  35677  connpconn  35727  cvmliftmolem2  35774  cvmlift2lem12  35806  poimirlem28  38319  fdc  38416  isbnd3  38455  pmap1N  40561  pol1N  40704  dia1N  41847  dihwN  42083  vdioph  43530  fiphp3d  43566  stirlinglem14  46821  fvmptrabdm  48050  suppdm  49310