Theorem rabeq0 4342

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∀wal 1540   = wceq 1542   ∈ wcel 2114  {cab 2715  ∀wral 3052  {crab 3401  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-ral 3053  df-rab 3402  df-dif 3906  df-nul 4288

This theorem is referenced by:  rabn0  4343  rabnc  4345  dffr2ALT  5594  wereu2  5629  frpomin  6306  frpomin2  6307  fndmdifeq0  6998  fnnfpeq0  7134  wemapso2  9470  wemapwe  9618  hashbclem  14387  hashbc  14388  wrdnfi  14483  smuval2  16421  smupvallem  16422  smu01lem  16424  smumullem  16431  phiprmpw  16715  hashgcdeq  16729  prmreclem4  16859  cshws0  17041  pmtrsn  19460  efgsfo  19680  00lsp  20944  ofldchr  21543  dsmm0cl  21707  ordthauslem  23339  pthaus  23594  xkohaus  23609  hmeofval  23714  mumul  27159  musum  27169  ppiub  27183  lgsquadlem2  27360  umgrnloop0  29194  lfgrnloop  29210  numedglnl  29229  usgrnloop0ALT  29290  lfuhgr1v0e  29339  nbuhgr  29428  nbumgr  29432  uhgrnbgr0nb  29439  nbgr0edglem  29441  vtxd0nedgb  29574  vtxdusgr0edgnelALT  29582  1loopgrnb0  29588  usgrvd0nedg  29619  vtxdginducedm1lem4  29628  wwlks  29920  iswwlksnon  29938  iswspthsnon  29941  0enwwlksnge1  29949  wspn0  30009  rusgr0edg  30061  clwwlk  30070  clwwlkn  30113  clwwlkn0  30115  clwwlknon  30177  clwwlknon1nloop  30186  clwwlknondisj  30198  vdn0conngrumgrv2  30283  eupth2lemb  30324  eulercrct  30329  frgrregorufr0  30411  numclwwlk3lem2  30471  esplyfval2  33742  2sqr3minply  33958  cos9thpiminply  33966  zarcls1  34047  measvuni  34392  dya2iocuni  34461  repr0  34789  reprlt  34797  reprgt  34799  nummin  35270  fineqvnttrclselem1  35299  subfacp1lem6  35401  prv1n  35647  poimirlem26  37897  poimirlem27  37898  cnambfre  37919  itg2addnclem2  37923  areacirclem5  37963  sticksstones1  42516  nna4b4nsq  43018  0dioph  43135  undisjrab  44662  supminfxr  45822  dvnprodlem3  46306  pimltmnf2f  47055  pimconstlt0  47059  pimgtpnf2f  47063  isubgr0uhgr  48233  stgr0  48320  rmsupp0  48728  lcoc0  48782  rrxsphere  49108