Theorem rabeq0 4387

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∀wal 1537   = wceq 1539   ∈ wcel 2107  {cab 2713  ∀wral 3060  {crab 3435  ∅c0 4332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2714  df-cleq 2728  df-ral 3061  df-rab 3436  df-dif 3953  df-nul 4333

This theorem is referenced by:  rabn0  4388  rabnc  4390  dffr2ALT  5646  wereu2  5681  frpomin  6360  frpomin2  6361  tz6.26OLD  6368  fndmdifeq0  7063  fnnfpeq0  7199  wemapso2  9594  wemapwe  9738  hashbclem  14492  hashbc  14493  wrdnfi  14587  smuval2  16520  smupvallem  16521  smu01lem  16523  smumullem  16530  phiprmpw  16814  hashgcdeq  16828  prmreclem4  16958  cshws0  17140  pmtrsn  19538  efgsfo  19758  00lsp  20980  dsmm0cl  21761  ordthauslem  23392  pthaus  23647  xkohaus  23662  hmeofval  23767  mumul  27225  musum  27235  ppiub  27249  lgsquadlem2  27426  umgrnloop0  29127  lfgrnloop  29143  numedglnl  29162  usgrnloop0ALT  29223  lfuhgr1v0e  29272  nbuhgr  29361  nbumgr  29365  uhgrnbgr0nb  29372  nbgr0edglem  29374  vtxd0nedgb  29507  vtxdusgr0edgnelALT  29515  1loopgrnb0  29521  usgrvd0nedg  29552  vtxdginducedm1lem4  29561  wwlks  29856  iswwlksnon  29874  iswspthsnon  29877  0enwwlksnge1  29885  wspn0  29945  rusgr0edg  29994  clwwlk  30003  clwwlkn  30046  clwwlkn0  30048  clwwlknon  30110  clwwlknon1nloop  30119  clwwlknondisj  30131  vdn0conngrumgrv2  30216  eupth2lemb  30257  eulercrct  30262  frgrregorufr0  30344  numclwwlk3lem2  30404  ofldchr  33345  2sqr3minply  33792  zarcls1  33869  measvuni  34216  dya2iocuni  34286  repr0  34627  reprlt  34635  reprgt  34637  nummin  35106  subfacp1lem6  35191  prv1n  35437  poimirlem26  37654  poimirlem27  37655  cnambfre  37676  itg2addnclem2  37680  areacirclem5  37720  sticksstones1  42148  nna4b4nsq  42675  0dioph  42794  undisjrab  44330  supminfxr  45480  dvnprodlem3  45968  pimltmnf2f  46717  pimconstlt0  46721  pimgtpnf2f  46725  isubgr0uhgr  47864  stgr0  47932  rmsupp0  48289  lcoc0  48344  rrxsphere  48674