Theorem rabeq0 4337

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401  ∀wal 1567   = wceq 1569   ∈ wcel 2144  {cab 2738  ∀wral 3076  {crab 3412  ∅c0 4277

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-ral 3077  df-rab 3413  df-dif 4046  df-nul 4278

This theorem is used by:  rabn0  4338  rabnc  4340  dffr2ALT  5613  wereu2  5648  frpomin  6346  frpomin2  6347  fndmdifeq0  7048  fnnfpeq0  7187  wemapso2  9554  wemapwe  9705  hashbclem  14604  hashbc  14605  wrdnfi  14700  smuval2  16661  smupvallem  16662  smu01lem  16664  smumullem  16671  phiprmpw  16962  hashgcdeq  16976  prmreclem4  17106  cshws0  17288  pmtrsn  19742  efgsfo  19962  00lsp  21265  ofldchr  21891  dsmm0cl  22055  ordthauslem  23710  pthaus  23966  xkohaus  23981  hmeofval  24086  mumul  27517  musum  27527  ppiub  27540  lgsquadlem2  27717  nna4b4nsq  27999  umgrnloop0  29696  lfgrnloop  29712  numedglnl  29731  usgrnloop0ALT  29795  lfuhgr1v0e  29844  nbuhgr  29933  nbumgr  29937  uhgrnbgr0nb  29944  nbgr0edglem  29946  vtxd0nedgb  30078  vtxdusgr0edgnelALT  30086  1loopgrnb0  30092  usgrvd0nedg  30123  vtxdginducedm1lem4  30132  wwlks  30433  iswwlksnon  30451  iswspthsnon  30454  0enwwlksnge1  30462  wspn0  30522  rusgr0edg  30574  clwwlk  30583  clwwlkn  30626  clwwlkn0  30628  clwwlknon  30690  clwwlknon1nloop  30699  clwwlknondisj  30711  vdn0conngrumgrv2  30806  eupth2lemb  30847  eulercrct  30852  frgrregorufr0  30934  numclwwlk3lem2  30994  esplyfval2  34247  2sqr3minply  34462  cos9thpiminply  34470  zarcls1  34551  measvuni  34897  dya2iocuni  34965  repr0  35290  reprlt  35298  reprgt  35300  nummin  35778  fineqvnttrclselem1  35849  subfacp1lem6  36040  prv1n  36286  poimirlem26  38673  poimirlem27  38674  cnambfre  38695  itg2addnclem2  38699  areacirclem5  38739  sticksstones1  43305  frlmnzcoordex  43761  0dioph  43898  undisjrab  45399  supminfxr  46582  dvnprodlem3  47066  pimltmnf2f  47815  pimconstlt0  47819  pimgtpnf2f  47823  isubgr0uhgr  49079  stgr0  49166  rmsupp0  49588  lcoc0  49642  rrxsphere  49968