Theorem rabeq0 4352

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 4343	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		df-rab 3424	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	2	eqeq1i 2774	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅)
4		raln 3094	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
5	1, 3, 4	3bitr4i 306	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 400  ∀wal 1565   = wceq 1567   ∈ wcel 2149  {cab 2747  ∀wral 3085  {crab 3423  ∅c0 4294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-ral 3086  df-rab 3424  df-dif 3916  df-nul 4295

This theorem is referenced by:  rabn0  4353  rabnc  4355  dffr2ALT  5624  wereu2  5659  frpomin  6342  frpomin2  6343  fndmdifeq0  7040  fnnfpeq0  7177  wemapso2  9514  wemapwe  9665  hashbclem  14488  hashbc  14489  wrdnfi  14584  smuval2  16539  smupvallem  16540  smu01lem  16542  smumullem  16549  phiprmpw  16834  hashgcdeq  16848  prmreclem4  16978  cshws0  17160  pmtrsn  19588  efgsfo  19808  00lsp  21079  ofldchr  21694  dsmm0cl  21858  ordthauslem  23508  pthaus  23763  xkohaus  23778  hmeofval  23883  mumul  27310  musum  27320  ppiub  27333  lgsquadlem2  27510  umgrnloop0  29399  lfgrnloop  29415  numedglnl  29434  usgrnloop0ALT  29495  lfuhgr1v0e  29544  nbuhgr  29633  nbumgr  29637  uhgrnbgr0nb  29644  nbgr0edglem  29646  vtxd0nedgb  29778  vtxdusgr0edgnelALT  29786  1loopgrnb0  29792  usgrvd0nedg  29823  vtxdginducedm1lem4  29832  wwlks  30124  iswwlksnon  30142  iswspthsnon  30145  0enwwlksnge1  30153  wspn0  30213  rusgr0edg  30265  clwwlk  30274  clwwlkn  30317  clwwlkn0  30319  clwwlknon  30381  clwwlknon1nloop  30390  clwwlknondisj  30402  vdn0conngrumgrv2  30487  eupth2lemb  30528  eulercrct  30533  frgrregorufr0  30615  numclwwlk3lem2  30675  esplyfval2  33899  2sqr3minply  34114  cos9thpiminply  34122  zarcls1  34203  measvuni  34548  dya2iocuni  34617  repr0  34942  reprlt  34950  reprgt  34952  nummin  35426  fineqvnttrclselem1  35456  subfacp1lem6  35575  prv1n  35821  poimirlem26  38184  poimirlem27  38185  cnambfre  38206  itg2addnclem2  38210  areacirclem5  38250  sticksstones1  42802  nna4b4nsq  43283  0dioph  43400  undisjrab  44907  supminfxr  46069  dvnprodlem3  46553  pimltmnf2f  47302  pimconstlt0  47306  pimgtpnf2f  47310  isubgr0uhgr  48526  stgr0  48613  rmsupp0  49032  lcoc0  49086  rrxsphere  49412