Theorem disj2 3724

Description: Two ways of saying that two classes are disjoint. (Contributed by NM, 17-May-1998.)

Assertion

Ref	Expression
disj2	|- ( ( A i^i B ) = (/) <-> A C_ ( _V \ B ) )

Proof of Theorem disj2

Step	Hyp	Ref	Expression
1		ssv 3374	. 2 |- A C_ _V
2		reldisj 3720	. 2 |- ( A C_ _V -> ( ( A i^i B ) = (/) <-> A C_ ( _V \ B ) ) )
3	1, 2	ax-mp 5	1 |- ( ( A i^i B ) = (/) <-> A C_ ( _V \ B ) )

Syntax hints:   <-> wb 184   = wceq 1369   _Vcvv 2970   \ cdif 3323   i^i cin 3325   C_ wss 3326   (/)c0 3635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718  df-v 2972  df-dif 3329  df-in 3333  df-ss 3340  df-nul 3636

This theorem is referenced by:  ssindif0  3730  intirr  5214  setsres  14200  setscom  14202  f1omvdco3  15953  psgnunilem5  15998  opsrtoslem2  17564  clscon  19032  cldsubg  19679  imadifxp  25937