Theorem rabeq0 4319

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 396  ∀wal 1537   = wceq 1539   ∈ wcel 2107  {cab 2716  ∀wral 3065  {crab 3069  ∅c0 4257

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2717  df-cleq 2731  df-ral 3070  df-rab 3074  df-dif 3891  df-nul 4258

This theorem is referenced by:  rabn0  4320  rabnc  4322  dffr2ALT  5555  wereu2  5587  frpomin  6247  frpomin2  6248  tz6.26OLD  6255  fndmdifeq0  6930  fnnfpeq0  7059  wemapso2  9321  wemapwe  9464  hashbclem  14173  hashbc  14174  wrdnfi  14260  smuval2  16198  smupvallem  16199  smu01lem  16201  smumullem  16208  phiprmpw  16486  hashgcdeq  16499  prmreclem4  16629  cshws0  16812  pmtrsn  19136  efgsfo  19354  00lsp  20252  dsmm0cl  20956  ordthauslem  22543  pthaus  22798  xkohaus  22813  hmeofval  22918  mumul  26339  musum  26349  ppiub  26361  lgsquadlem2  26538  umgrnloop0  27488  lfgrnloop  27504  numedglnl  27523  usgrnloop0ALT  27581  lfuhgr1v0e  27630  nbuhgr  27719  nbumgr  27723  uhgrnbgr0nb  27730  nbgr0vtxlem  27731  vtxd0nedgb  27864  vtxdusgr0edgnelALT  27872  1loopgrnb0  27878  usgrvd0nedg  27909  vtxdginducedm1lem4  27918  wwlks  28209  iswwlksnon  28227  iswspthsnon  28230  0enwwlksnge1  28238  wspn0  28298  rusgr0edg  28347  clwwlk  28356  clwwlkn  28399  clwwlkn0  28401  clwwlknon  28463  clwwlknon1nloop  28472  clwwlknondisj  28484  vdn0conngrumgrv2  28569  eupth2lemb  28610  eulercrct  28615  frgrregorufr0  28697  numclwwlk3lem2  28757  ofldchr  31522  zarcls1  31828  measvuni  32191  dya2iocuni  32259  repr0  32600  reprlt  32608  reprgt  32610  nummin  33072  subfacp1lem6  33156  prv1n  33402  poimirlem26  35812  poimirlem27  35813  cnambfre  35834  itg2addnclem2  35838  areacirclem5  35878  sticksstones1  40109  nna4b4nsq  40504  0dioph  40607  undisjrab  41931  supminfxr  43011  dvnprodlem3  43496  pimltmnf2f  44242  pimconstlt0  44246  pimgtpnf2f  44250  rmsupp0  45715  lcoc0  45774  rrxsphere  46105