Theorem rabid2 3478

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

Syntax hints:   ↔ wb 206   = wceq 1537  ∀wral 3067  {crab 3443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rab 3444

This theorem is referenced by:  iinrab2  5093  riinrab  5107  dmmptg  6273  frpoinsg  6375  wfisgOLD  6386  dmmptd  6725  fneqeql  7079  fmpt  7144  tfisg  7891  zfrep6  7995  frinsg  9820  axdc2lem  10517  ioomax  13482  iccmax  13483  hashbc  14502  lcmf0  16681  dfphi2  16821  phiprmpw  16823  phisum  16837  isnsg4  19207  symggen2  19513  psgnfvalfi  19555  lssuni  20960  psgnghm2  21622  ocv0  21718  dsmmfi  21781  frlmfibas  21805  frlmlbs  21840  psr1baslem  22207  ordtrest2lem  23232  comppfsc  23561  xkouni  23628  xkoccn  23648  tsmsfbas  24157  clsocv  25303  ehlbase  25468  ovolicc2lem4  25574  itg2monolem1  25805  musum  27252  lgsquadlem2  27443  umgr2v2evd2  29563  frgrregorufr0  30356  ubthlem1  30902  xrsclat  32994  psgndmfi  33091  primefldgen1  33288  zarcls0  33814  ordtrest2NEWlem  33868  hasheuni  34049  measvuni  34178  imambfm  34227  subfacp1lem6  35153  connpconn  35203  cvmliftmolem2  35250  cvmlift2lem12  35282  poimirlem28  37608  fdc  37705  isbnd3  37744  pmap1N  39724  pol1N  39867  dia1N  41010  dihwN  41246  vdioph  42735  fiphp3d  42775  stirlinglem14  46008  fvmptrabdm  47208  suppdm  48239