Theorem rabeq0 4339

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 4331	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		df-rab 3395	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	2	eqeq1i 2734	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅)
4		raln 3052	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
5	1, 3, 4	3bitr4i 303	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540   ∈ wcel 2109  {cab 2707  ∀wral 3044  {crab 3394  ∅c0 4284

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-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-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-ral 3045  df-rab 3395  df-dif 3906  df-nul 4285

This theorem is referenced by:  rabn0  4340  rabnc  4342  dffr2ALT  5581  wereu2  5616  frpomin  6288  frpomin2  6289  fndmdifeq0  6978  fnnfpeq0  7114  wemapso2  9445  wemapwe  9593  hashbclem  14359  hashbc  14360  wrdnfi  14455  smuval2  16393  smupvallem  16394  smu01lem  16396  smumullem  16403  phiprmpw  16687  hashgcdeq  16701  prmreclem4  16831  cshws0  17013  pmtrsn  19398  efgsfo  19618  00lsp  20884  ofldchr  21483  dsmm0cl  21647  ordthauslem  23268  pthaus  23523  xkohaus  23538  hmeofval  23643  mumul  27089  musum  27099  ppiub  27113  lgsquadlem2  27290  umgrnloop0  29054  lfgrnloop  29070  numedglnl  29089  usgrnloop0ALT  29150  lfuhgr1v0e  29199  nbuhgr  29288  nbumgr  29292  uhgrnbgr0nb  29299  nbgr0edglem  29301  vtxd0nedgb  29434  vtxdusgr0edgnelALT  29442  1loopgrnb0  29448  usgrvd0nedg  29479  vtxdginducedm1lem4  29488  wwlks  29780  iswwlksnon  29798  iswspthsnon  29801  0enwwlksnge1  29809  wspn0  29869  rusgr0edg  29918  clwwlk  29927  clwwlkn  29970  clwwlkn0  29972  clwwlknon  30034  clwwlknon1nloop  30043  clwwlknondisj  30055  vdn0conngrumgrv2  30140  eupth2lemb  30181  eulercrct  30186  frgrregorufr0  30268  numclwwlk3lem2  30328  2sqr3minply  33747  cos9thpiminply  33755  zarcls1  33836  measvuni  34181  dya2iocuni  34251  repr0  34579  reprlt  34587  reprgt  34589  nummin  35058  subfacp1lem6  35158  prv1n  35404  poimirlem26  37626  poimirlem27  37627  cnambfre  37648  itg2addnclem2  37652  areacirclem5  37692  sticksstones1  42119  nna4b4nsq  42633  0dioph  42751  undisjrab  44279  supminfxr  45443  dvnprodlem3  45929  pimltmnf2f  46678  pimconstlt0  46682  pimgtpnf2f  46686  isubgr0uhgr  47857  stgr0  47944  rmsupp0  48352  lcoc0  48407  rrxsphere  48733