Theorem rabeq0 4335

Description: Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010.) (Revised by BJ, 16-Jul-2021.)

Assertion

Ref	Expression
rabeq0	⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Proof of Theorem rabeq0

Step	Hyp	Ref	Expression
1		ab0 4327	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		df-rab 3396	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	2	eqeq1i 2736	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅)
4		raln 3055	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
5	1, 3, 4	3bitr4i 303	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541   ∈ wcel 2111  {cab 2709  ∀wral 3047  {crab 3395  ∅c0 4280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-ral 3048  df-rab 3396  df-dif 3900  df-nul 4281

This theorem is referenced by:  rabn0  4336  rabnc  4338  dffr2ALT  5576  wereu2  5611  frpomin  6287  frpomin2  6288  fndmdifeq0  6977  fnnfpeq0  7112  wemapso2  9439  wemapwe  9587  hashbclem  14359  hashbc  14360  wrdnfi  14455  smuval2  16393  smupvallem  16394  smu01lem  16396  smumullem  16403  phiprmpw  16687  hashgcdeq  16701  prmreclem4  16831  cshws0  17013  pmtrsn  19431  efgsfo  19651  00lsp  20914  ofldchr  21513  dsmm0cl  21677  ordthauslem  23298  pthaus  23553  xkohaus  23568  hmeofval  23673  mumul  27118  musum  27128  ppiub  27142  lgsquadlem2  27319  umgrnloop0  29087  lfgrnloop  29103  numedglnl  29122  usgrnloop0ALT  29183  lfuhgr1v0e  29232  nbuhgr  29321  nbumgr  29325  uhgrnbgr0nb  29332  nbgr0edglem  29334  vtxd0nedgb  29467  vtxdusgr0edgnelALT  29475  1loopgrnb0  29481  usgrvd0nedg  29512  vtxdginducedm1lem4  29521  wwlks  29813  iswwlksnon  29831  iswspthsnon  29834  0enwwlksnge1  29842  wspn0  29902  rusgr0edg  29954  clwwlk  29963  clwwlkn  30006  clwwlkn0  30008  clwwlknon  30070  clwwlknon1nloop  30079  clwwlknondisj  30091  vdn0conngrumgrv2  30176  eupth2lemb  30217  eulercrct  30222  frgrregorufr0  30304  numclwwlk3lem2  30364  2sqr3minply  33793  cos9thpiminply  33801  zarcls1  33882  measvuni  34227  dya2iocuni  34296  repr0  34624  reprlt  34632  reprgt  34634  nummin  35104  fineqvnttrclselem1  35141  subfacp1lem6  35229  prv1n  35475  poimirlem26  37694  poimirlem27  37695  cnambfre  37716  itg2addnclem2  37720  areacirclem5  37760  sticksstones1  42187  nna4b4nsq  42701  0dioph  42819  undisjrab  44347  supminfxr  45510  dvnprodlem3  45994  pimltmnf2f  46743  pimconstlt0  46747  pimgtpnf2f  46751  isubgr0uhgr  47912  stgr0  47999  rmsupp0  48407  lcoc0  48462  rrxsphere  48788