Theorem rabeq0 4328

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∀wal 1540   = wceq 1542   ∈ wcel 2114  {cab 2714  ∀wral 3051  {crab 3389  ∅c0 4273

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 2708

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 2715  df-cleq 2728  df-ral 3052  df-rab 3390  df-dif 3892  df-nul 4274

This theorem is referenced by:  rabn0  4329  rabnc  4331  dffr2ALT  5593  wereu2  5628  frpomin  6304  frpomin2  6305  fndmdifeq0  6996  fnnfpeq0  7133  wemapso2  9468  wemapwe  9618  hashbclem  14414  hashbc  14415  wrdnfi  14510  smuval2  16451  smupvallem  16452  smu01lem  16454  smumullem  16461  phiprmpw  16746  hashgcdeq  16760  prmreclem4  16890  cshws0  17072  pmtrsn  19494  efgsfo  19714  00lsp  20976  ofldchr  21556  dsmm0cl  21720  ordthauslem  23348  pthaus  23603  xkohaus  23618  hmeofval  23723  mumul  27144  musum  27154  ppiub  27167  lgsquadlem2  27344  umgrnloop0  29178  lfgrnloop  29194  numedglnl  29213  usgrnloop0ALT  29274  lfuhgr1v0e  29323  nbuhgr  29412  nbumgr  29416  uhgrnbgr0nb  29423  nbgr0edglem  29425  vtxd0nedgb  29557  vtxdusgr0edgnelALT  29565  1loopgrnb0  29571  usgrvd0nedg  29602  vtxdginducedm1lem4  29611  wwlks  29903  iswwlksnon  29921  iswspthsnon  29924  0enwwlksnge1  29932  wspn0  29992  rusgr0edg  30044  clwwlk  30053  clwwlkn  30096  clwwlkn0  30098  clwwlknon  30160  clwwlknon1nloop  30169  clwwlknondisj  30181  vdn0conngrumgrv2  30266  eupth2lemb  30307  eulercrct  30312  frgrregorufr0  30394  numclwwlk3lem2  30454  esplyfval2  33709  2sqr3minply  33924  cos9thpiminply  33932  zarcls1  34013  measvuni  34358  dya2iocuni  34427  repr0  34755  reprlt  34763  reprgt  34765  nummin  35236  fineqvnttrclselem1  35265  subfacp1lem6  35367  prv1n  35613  poimirlem26  37967  poimirlem27  37968  cnambfre  37989  itg2addnclem2  37993  areacirclem5  38033  sticksstones1  42585  nna4b4nsq  43093  0dioph  43210  undisjrab  44733  supminfxr  45892  dvnprodlem3  46376  pimltmnf2f  47125  pimconstlt0  47129  pimgtpnf2f  47133  isubgr0uhgr  48349  stgr0  48436  rmsupp0  48844  lcoc0  48898  rrxsphere  49224