Theorem rabid2 3472

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

Syntax hints:   ↔ wb 206   = wceq 1537  ∀wral 3063  {crab 3438

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 2105  ax-9 2113  ax-10 2136  ax-11 2153  ax-12 2173  ax-ext 2705

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 2712  df-cleq 2726  df-clel 2813  df-nfc 2890  df-ral 3064  df-rab 3439

This theorem is referenced by:  iinrab2  5096  riinrab  5110  dmmptg  6272  frpoinsg  6374  wfisgOLD  6385  dmmptd  6724  fneqeql  7077  fmpt  7142  tfisg  7887  zfrep6  7991  frinsg  9816  axdc2lem  10513  ioomax  13478  iccmax  13479  hashbc  14498  lcmf0  16675  dfphi2  16816  phiprmpw  16818  phisum  16832  isnsg4  19202  symggen2  19508  psgnfvalfi  19550  lssuni  20955  psgnghm2  21617  ocv0  21713  dsmmfi  21776  frlmfibas  21800  frlmlbs  21835  psr1baslem  22200  ordtrest2lem  23225  comppfsc  23554  xkouni  23621  xkoccn  23641  tsmsfbas  24150  clsocv  25296  ehlbase  25461  ovolicc2lem4  25567  itg2monolem1  25798  musum  27243  lgsquadlem2  27434  umgr2v2evd2  29554  frgrregorufr0  30347  ubthlem1  30893  xrsclat  32986  psgndmfi  33083  primefldgen1  33280  zarcls0  33806  ordtrest2NEWlem  33860  hasheuni  34041  measvuni  34170  imambfm  34219  subfacp1lem6  35145  connpconn  35195  cvmliftmolem2  35242  cvmlift2lem12  35274  poimirlem28  37556  fdc  37653  isbnd3  37692  pmap1N  39672  pol1N  39815  dia1N  40958  dihwN  41194  vdioph  42672  fiphp3d  42712  stirlinglem14  45942  fvmptrabdm  47140  suppdm  48157