Theorem rabid2 3436

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

Syntax hints:   ↔ wb 206   = wceq 1540  ∀wral 3044  {crab 3402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rab 3403

This theorem is referenced by:  iinrab2  5029  riinrab  5043  dmmptg  6203  frpoinsg  6304  dmmptd  6645  fneqeql  7000  fmpt  7064  tfisg  7810  zfrep6  7913  frinsg  9680  axdc2lem  10377  ioomax  13359  iccmax  13360  hashbc  14394  lcmf0  16580  dfphi2  16720  phiprmpw  16722  phisum  16737  isnsg4  19081  symggen2  19385  psgnfvalfi  19427  lssuni  20877  psgnghm2  21523  ocv0  21619  dsmmfi  21680  frlmfibas  21704  frlmlbs  21739  psr1baslem  22102  ordtrest2lem  23123  comppfsc  23452  xkouni  23519  xkoccn  23539  tsmsfbas  24048  clsocv  25183  ehlbase  25348  ovolicc2lem4  25454  itg2monolem1  25684  musum  27134  lgsquadlem2  27325  umgr2v2evd2  29508  frgrregorufr0  30303  ubthlem1  30849  xrsclat  32995  psgndmfi  33070  primefldgen1  33287  zarcls0  33851  ordtrest2NEWlem  33905  hasheuni  34068  measvuni  34197  imambfm  34246  subfacp1lem6  35165  connpconn  35215  cvmliftmolem2  35262  cvmlift2lem12  35294  poimirlem28  37635  fdc  37732  isbnd3  37771  pmap1N  39754  pol1N  39897  dia1N  41040  dihwN  41276  vdioph  42760  fiphp3d  42800  stirlinglem14  46078  fvmptrabdm  47287  suppdm  48492