Proofgold Address

Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Known TrueI^TrueI : True
Theorem bbee1..^tab_neg_True : not True ⟶ False (proof)
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem f6404..^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2 (proof)
Known and_def^and_def : and = λ x1 x2 : ο . ∀ x3 : ο . (x1 ⟶ x2 ⟶ x3) ⟶ x3
Theorem cd094..^and3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3) ⟶ x3 (proof)
Known dcbd9..^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Theorem cb243..^or3I1 : ∀ x0 x1 x2 : ο . x0 ⟶ or (or x0 x1) x2 (proof)
Known eca40..^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem 8aff3..^or3I2 : ∀ x0 x1 x2 : ο . x1 ⟶ or (or x0 x1) x2 (proof)
Theorem a4277..^or3I3 : ∀ x0 x1 x2 : ο . x2 ⟶ or (or x0 x1) x2 (proof)
Known f13f4..^or_def : or = λ x1 x2 : ο . ∀ x3 : ο . (x1 ⟶ x3) ⟶ (x2 ⟶ x3) ⟶ x3
Theorem 8cb38..^or3E : ∀ x0 x1 x2 : ο . or (or x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x3) ⟶ (x1 ⟶ x3) ⟶ (x2 ⟶ x3) ⟶ x3 (proof)
Theorem 22d81..^and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3 (proof)
Theorem a660e..^and4E : ∀ x0 x1 x2 x3 : ο . and (and (and x0 x1) x2) x3 ⟶ ∀ x4 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4) ⟶ x4 (proof)
Theorem 266ab..^or4I1 : ∀ x0 x1 x2 x3 : ο . x0 ⟶ or (or (or x0 x1) x2) x3 (proof)
Theorem 0675f..^or4I2 : ∀ x0 x1 x2 x3 : ο . x1 ⟶ or (or (or x0 x1) x2) x3 (proof)
Theorem e3915..^or4I3 : ∀ x0 x1 x2 x3 : ο . x2 ⟶ or (or (or x0 x1) x2) x3 (proof)
Theorem 4354d..^or4I4 : ∀ x0 x1 x2 x3 : ο . x3 ⟶ or (or (or x0 x1) x2) x3 (proof)
Theorem c3778..^or4E : ∀ x0 x1 x2 x3 : ο . or (or (or x0 x1) x2) x3 ⟶ ∀ x4 : ο . (x0 ⟶ x4) ⟶ (x1 ⟶ x4) ⟶ (x2 ⟶ x4) ⟶ (x3 ⟶ x4) ⟶ x4 (proof)
Theorem 1bd08..^and5I : ∀ x0 x1 x2 x3 x4 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ and (and (and (and x0 x1) x2) x3) x4 (proof)
Theorem d5e32..^and5E : ∀ x0 x1 x2 x3 x4 : ο . and (and (and (and x0 x1) x2) x3) x4 ⟶ ∀ x5 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5) ⟶ x5 (proof)
Theorem 17f0e..^or5I1 : ∀ x0 x1 x2 x3 x4 : ο . x0 ⟶ or (or (or (or x0 x1) x2) x3) x4 (proof)
Theorem a13f5..^or5I2 : ∀ x0 x1 x2 x3 x4 : ο . x1 ⟶ or (or (or (or x0 x1) x2) x3) x4 (proof)
Theorem 864e8..^or5I3 : ∀ x0 x1 x2 x3 x4 : ο . x2 ⟶ or (or (or (or x0 x1) x2) x3) x4 (proof)
Theorem 389cb..^or5I4 : ∀ x0 x1 x2 x3 x4 : ο . x3 ⟶ or (or (or (or x0 x1) x2) x3) x4 (proof)
Theorem 75472..^or5I5 : ∀ x0 x1 x2 x3 x4 : ο . x4 ⟶ or (or (or (or x0 x1) x2) x3) x4 (proof)
Theorem 46520..^or5E : ∀ x0 x1 x2 x3 x4 : ο . or (or (or (or x0 x1) x2) x3) x4 ⟶ ∀ x5 : ο . (x0 ⟶ x5) ⟶ (x1 ⟶ x5) ⟶ (x2 ⟶ x5) ⟶ (x3 ⟶ x5) ⟶ (x4 ⟶ x5) ⟶ x5 (proof)
Theorem fc6fc..^and6I : ∀ x0 x1 x2 x3 x4 x5 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ and (and (and (and (and x0 x1) x2) x3) x4) x5 (proof)
Theorem 6130e..^and6E : ∀ x0 x1 x2 x3 x4 x5 : ο . and (and (and (and (and x0 x1) x2) x3) x4) x5 ⟶ ∀ x6 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6) ⟶ x6 (proof)
Theorem 92342..^and7I : ∀ x0 x1 x2 x3 x4 x5 x6 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6 (proof)
Theorem dd249..^and7E : ∀ x0 x1 x2 x3 x4 x5 x6 : ο . and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6 ⟶ ∀ x7 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7) ⟶ x7 (proof)
Known b4782..^contra : ∀ x0 : ο . (not x0 ⟶ False) ⟶ x0
Theorem ae2b8..^tab_neg_ex_i : ∀ x0 : ι → ο . ∀ x1 . not (∀ x2 : ο . (∀ x3 . x0 x3 ⟶ x2) ⟶ x2) ⟶ (not (x0 x1) ⟶ False) ⟶ False (proof)
Known 4cb75..^Eps_i_R : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ x0 (Eps_i x0)
Theorem Eps_i_ex^Eps_i_R2 : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (Eps_i x0) (proof)
Known 47706..^xmcases : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (not x0 ⟶ x1) ⟶ x1
Known 6abef..^nIn_I : ∀ x0 x1 . not (In x0 x1) ⟶ nIn x0 x1
Theorem 3ab01..^xmcases_In : ∀ x0 x1 . ∀ x2 : ο . (In x0 x1 ⟶ x2) ⟶ (nIn x0 x1 ⟶ x2) ⟶ x2 (proof)
Known 4f094..^Sep_def : Sep = λ x1 . λ x2 : ι → ο . If_i (∀ x3 : ο . (∀ x4 . and (In x4 x1) (x2 x4) ⟶ x3) ⟶ x3) (Repl x1 (λ x3 . If_i (x2 x3) x3 (Eps_i (λ x4 . and (In x4 x1) (x2 x4))))) 0
Known f1bf4..^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 x0 ⟶ In (x1 x2) (Repl x0 x1)
Known 0d2f9..^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Theorem dab1f..^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . In x2 x0 ⟶ x1 x2 ⟶ In x2 (Sep x0 x1) (proof)
Known 0f096..^ReplE2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (Repl x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . In x4 x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known 81513..^If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known 2901c..^EmptyE : ∀ x0 . In x0 0 ⟶ False
Theorem c967f..^SepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . In x2 (Sep x0 x1) ⟶ and (In x2 x0) (x1 x2) (proof)
Known andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem aa3f4..^SepE_impred : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . In x2 (Sep x0 x1) ⟶ ∀ x3 : ο . (In x2 x0 ⟶ x1 x2 ⟶ x3) ⟶ x3 (proof)
Theorem c4260..^SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . In x2 (Sep x0 x1) ⟶ In x2 x0 (proof)
Theorem 076ba..^SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . In x2 (Sep x0 x1) ⟶ x1 x2 (proof)
Known b0dce..^SubqI : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ Subq x0 x1
Theorem d05a3..^Sep_Subq : ∀ x0 . ∀ x1 : ι → ο . Subq (Sep x0 x1) x0 (proof)
Known 2d44a..^PowerI : ∀ x0 x1 . Subq x1 x0 ⟶ In x1 (Power x0)
Theorem fa8b5..^Sep_In_Power : ∀ x0 . ∀ x1 : ι → ο . In (Sep x0 x1) (Power x0) (proof)
Theorem 34fe8..^tab_pos_Sep : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . In x2 (Sep x0 x1) ⟶ (In x2 x0 ⟶ x1 x2 ⟶ False) ⟶ False (proof)
Known 24526..^nIn_E2 : ∀ x0 x1 . nIn x0 x1 ⟶ In x0 x1 ⟶ False
Known 085e3..^contra_In : ∀ x0 x1 . (nIn x0 x1 ⟶ False) ⟶ In x0 x1
Theorem 49d23..^tab_neg_Sep : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . nIn x2 (Sep x0 x1) ⟶ (nIn x2 x0 ⟶ False) ⟶ (not (x1 x2) ⟶ False) ⟶ False (proof)
Known f88cc..^ReplSep_def : ReplSep = λ x1 . λ x2 : ι → ο . Repl (Sep x1 x2)
Theorem 9fdc4..^ReplSepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . In x3 x0 ⟶ x1 x3 ⟶ In (x2 x3) (ReplSep x0 x1 x2) (proof)
Theorem 71143..^ReplSepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . In x3 (ReplSep x0 x1 x2) ⟶ ∀ x4 : ο . (∀ x5 . and (and (In x5 x0) (x1 x5)) (x3 = x2 x5) ⟶ x4) ⟶ x4 (proof)
Known 61640..^exandE_i : ∀ x0 x1 : ι → ο . (∀ x2 : ο . (∀ x3 . and (x0 x3) (x1 x3) ⟶ x2) ⟶ x2) ⟶ ∀ x2 : ο . (∀ x3 . x0 x3 ⟶ x1 x3 ⟶ x2) ⟶ x2
Theorem 65d0d..^{ReplSepE_impred} : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . In x3 (ReplSep x0 x1 x2) ⟶ ∀ x4 : ο . (∀ x5 . In x5 x0 ⟶ x1 x5 ⟶ x3 = x2 x5 ⟶ x4) ⟶ x4 (proof)
Theorem aeb4e..^{tab_pos_ReplSep} : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 . In x3 (ReplSep x0 x1 x2) ⟶ (∀ x4 . In x4 x0 ⟶ x1 x4 ⟶ x3 = x2 x4 ⟶ False) ⟶ False (proof)
Theorem c3612..^{tab_neg_ReplSep} : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 : ι → ι . ∀ x3 x4 . nIn x3 (ReplSep x0 x1 x2) ⟶ (nIn x4 x0 ⟶ False) ⟶ (not (x1 x4) ⟶ False) ⟶ (not (x3 = x2 x4) ⟶ False) ⟶ False (proof)
Known 535f2..^set_ext_2 : ∀ x0 x1 . (∀ x2 . In x2 x0 ⟶ In x2 x1) ⟶ (∀ x2 . In x2 x1 ⟶ In x2 x0) ⟶ x0 = x1
Known f9974..^{binunionE_cases} : ∀ x0 x1 x2 . In x2 (binunion x0 x1) ⟶ ∀ x3 : ο . (In x2 x0 ⟶ x3) ⟶ (In x2 x1 ⟶ x3) ⟶ x3
Known 0ce8c..^binunionI1 : ∀ x0 x1 x2 . In x2 x0 ⟶ In x2 (binunion x0 x1)
Known eb8b4..^binunionI2 : ∀ x0 x1 x2 . In x2 x1 ⟶ In x2 (binunion x0 x1)
Theorem 50617..^{binunion_asso} : ∀ x0 x1 x2 . binunion x0 (binunion x1 x2) = binunion (binunion x0 x1) x2 (proof)
Theorem a8a0c.. : ∀ x0 x1 . Subq (binunion x0 x1) (binunion x1 x0) (proof)
Known b3824..^set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Theorem 78b78..^binunion_com : ∀ x0 x1 . binunion x0 x1 = binunion x1 x0 (proof)
Theorem dae53..^binunion_idl : ∀ x0 . binunion 0 x0 = x0 (proof)
Theorem 70cfd..^binunion_idr : ∀ x0 . binunion x0 0 = x0 (proof)
Theorem 58eb6..^{binunion_idem} : ∀ x0 . binunion x0 x0 = x0 (proof)
Theorem 7570e..^{binunion_Subq_1} : ∀ x0 x1 . Subq x0 (binunion x0 x1) (proof)
Theorem de882..^{binunion_Subq_2} : ∀ x0 x1 . Subq x1 (binunion x0 x1) (proof)
Known c1173..^Subq_def : Subq = λ x1 x2 . ∀ x3 . In x3 x1 ⟶ In x3 x2
Theorem 75230..^{binunion_Subq_min} : ∀ x0 x1 x2 . Subq x0 x2 ⟶ Subq x1 x2 ⟶ Subq (binunion x0 x1) x2 (proof)
Known prop_ext_2^prop_ext_2 : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ x0 = x1
Known 6696a..^Subq_ref : ∀ x0 . Subq x0 x0
Theorem 69c3f..^{Subq_binunion_eq} : ∀ x0 x1 . Subq x0 x1 = (binunion x0 x1 = x1) (proof)
Known 9d2e6..^nIn_I2 : ∀ x0 x1 . (In x0 x1 ⟶ False) ⟶ nIn x0 x1
Theorem d22e3..^{binunion_nIn_I} : ∀ x0 x1 x2 . nIn x2 x0 ⟶ nIn x2 x1 ⟶ nIn x2 (binunion x0 x1) (proof)
Theorem 68d17..^{binunion_nIn_E} : ∀ x0 x1 x2 . nIn x2 (binunion x0 x1) ⟶ and (nIn x2 x0) (nIn x2 x1) (proof)
Theorem 17efc..^{binunion_nIn_E_impred} : ∀ x0 x1 x2 . nIn x2 (binunion x0 x1) ⟶ ∀ x3 : ο . (nIn x2 x0 ⟶ nIn x2 x1 ⟶ x3) ⟶ x3 (proof)
Known 52527..^{binintersect_def} : binintersect = λ x1 x2 . Sep x1 (λ x3 . In x3 x2)
Theorem dd25c..^{binintersectI} : ∀ x0 x1 x2 . In x2 x0 ⟶ In x2 x1 ⟶ In x2 (binintersect x0 x1) (proof)
Theorem 277ae..^{binintersectE} : ∀ x0 x1 x2 . In x2 (binintersect x0 x1) ⟶ and (In x2 x0) (In x2 x1) (proof)
Theorem 9c451..^{binintersectE_impred} : ∀ x0 x1 x2 . In x2 (binintersect x0 x1) ⟶ ∀ x3 : ο . (In x2 x0 ⟶ In x2 x1 ⟶ x3) ⟶ x3 (proof)
Theorem c5fa0..^{binintersectE1} : ∀ x0 x1 x2 . In x2 (binintersect x0 x1) ⟶ In x2 x0 (proof)
Theorem 5317c..^{binintersectE2} : ∀ x0 x1 x2 . In x2 (binintersect x0 x1) ⟶ In x2 x1 (proof)
Theorem 05c0a..^{binintersect_Subq_1} : ∀ x0 x1 . Subq (binintersect x0 x1) x0 (proof)
Theorem df480..^{binintersect_Subq_2} : ∀ x0 x1 . Subq (binintersect x0 x1) x1 (proof)
Known 367e6..^SubqE : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 . In x2 x0 ⟶ In x2 x1
Theorem 485cd..^{binintersect_Subq_eq_1} : ∀ x0 x1 . Subq x0 x1 ⟶ binintersect x0 x1 = x0 (proof)
Theorem b962e..^{binintersect_Subq_max} : ∀ x0 x1 x2 . Subq x2 x0 ⟶ Subq x2 x1 ⟶ Subq x2 (binintersect x0 x1) (proof)
Known 2ad64..^Subq_tra : ∀ x0 x1 x2 . Subq x0 x1 ⟶ Subq x1 x2 ⟶ Subq x0 x2
Theorem 0964f..^{binintersect_asso} : ∀ x0 x1 x2 . binintersect x0 (binintersect x1 x2) = binintersect (binintersect x0 x1) x2 (proof)
Theorem f946b.. : ∀ x0 x1 . Subq (binintersect x0 x1) (binintersect x1 x0) (proof)
Theorem 6b560..^{binintersect_com} : ∀ x0 x1 . binintersect x0 x1 = binintersect x1 x0 (proof)
Known d6778..^{Empty_Subq_eq} : ∀ x0 . Subq x0 0 ⟶ x0 = 0
Theorem ef0ec..^{binintersect_annil} : ∀ x0 . binintersect 0 x0 = 0 (proof)
Theorem a46a3..^{binintersect_annir} : ∀ x0 . binintersect x0 0 = 0 (proof)
Theorem 8ca5a..^{binintersect_idem} : ∀ x0 . binintersect x0 x0 = x0 (proof)
Theorem f1349..^{binintersect_binunion_distr} : ∀ x0 x1 x2 . binintersect x0 (binunion x1 x2) = binunion (binintersect x0 x1) (binintersect x0 x2) (proof)
Theorem 12c26..^{binunion_binintersect_distr} : ∀ x0 x1 x2 . binunion x0 (binintersect x1 x2) = binintersect (binunion x0 x1) (binunion x0 x2) (proof)
Theorem 5e05c..^{Subq_binintersection_eq} : ∀ x0 x1 . Subq x0 x1 = (binintersect x0 x1 = x0) (proof)
Theorem d11f4..^{binintersect_nIn_I1} : ∀ x0 x1 x2 . nIn x2 x0 ⟶ nIn x2 (binintersect x0 x1) (proof)
Theorem 4c3a8..^{binintersect_nIn_I2} : ∀ x0 x1 x2 . nIn x2 x1 ⟶ nIn x2 (binintersect x0 x1) (proof)
Theorem d7630..^{binintersect_nIn_E} : ∀ x0 x1 x2 . nIn x2 (binintersect x0 x1) ⟶ or (nIn x2 x0) (nIn x2 x1) (proof)
Known 37124..^orE : ∀ x0 x1 : ο . or x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Theorem 1ac88..^{binintersect_nIn_E_impred} : ∀ x0 x1 x2 . nIn x2 (binintersect x0 x1) ⟶ ∀ x3 : ο . (nIn x2 x0 ⟶ x3) ⟶ (nIn x2 x1 ⟶ x3) ⟶ x3 (proof)
Theorem 5d6fd..^{tab_pos_binintersect} : ∀ x0 x1 x2 . In x2 (binintersect x0 x1) ⟶ (In x2 x0 ⟶ In x2 x1 ⟶ False) ⟶ False (proof)
Theorem 30a90..^{tab_neg_binintersect} : ∀ x0 x1 x2 . nIn x2 (binintersect x0 x1) ⟶ (nIn x2 x0 ⟶ False) ⟶ (nIn x2 x1 ⟶ False) ⟶ False (proof)
Known f5588..^setminus_def : setminus = λ x1 x2 . Sep x1 (λ x3 . nIn x3 x2)
Theorem 626dc..^setminusI : ∀ x0 x1 x2 . In x2 x0 ⟶ nIn x2 x1 ⟶ In x2 (setminus x0 x1) (proof)
Theorem 349f7..^setminusE : ∀ x0 x1 x2 . In x2 (setminus x0 x1) ⟶ and (In x2 x0) (nIn x2 x1) (proof)
Theorem 243aa..^{setminusE_impred} : ∀ x0 x1 x2 . In x2 (setminus x0 x1) ⟶ ∀ x3 : ο . (In x2 x0 ⟶ nIn x2 x1 ⟶ x3) ⟶ x3 (proof)
Theorem 54d83..^setminusE1 : ∀ x0 x1 x2 . In x2 (setminus x0 x1) ⟶ In x2 x0 (proof)
Theorem 28403..^setminusE2 : ∀ x0 x1 x2 . In x2 (setminus x0 x1) ⟶ nIn x2 x1 (proof)
Theorem 74206..^{setminus_Subq} : ∀ x0 x1 . Subq (setminus x0 x1) x0 (proof)
Known a7ffa..^Subq_contra : ∀ x0 x1 x2 . Subq x0 x1 ⟶ nIn x2 x1 ⟶ nIn x2 x0
Theorem 8b73d..^{setminus_Subq_contra} : ∀ x0 x1 x2 . Subq x2 x1 ⟶ Subq (setminus x0 x1) (setminus x0 x2) (proof)
Theorem 6502f..^{setminus_nIn_I1} : ∀ x0 x1 x2 . nIn x2 x0 ⟶ nIn x2 (setminus x0 x1) (proof)
Theorem 6d89c..^{setminus_nIn_I2} : ∀ x0 x1 x2 . In x2 x1 ⟶ nIn x2 (setminus x0 x1) (proof)
Theorem 2c30c..^{setminus_nIn_E} : ∀ x0 x1 x2 . nIn x2 (setminus x0 x1) ⟶ or (nIn x2 x0) (In x2 x1) (proof)
Theorem af072..^{setminus_nIn_E_impred} : ∀ x0 x1 x2 . nIn x2 (setminus x0 x1) ⟶ ∀ x3 : ο . (nIn x2 x0 ⟶ x3) ⟶ (In x2 x1 ⟶ x3) ⟶ x3 (proof)
Known d0de4..^Empty_eq : ∀ x0 . (∀ x1 . nIn x1 x0) ⟶ x0 = 0
Theorem 24940..^{setminus_selfannih} : ∀ x0 . setminus x0 x0 = 0 (proof)
Theorem a43ed..^{setminus_binintersect} : ∀ x0 x1 x2 . setminus x0 (binintersect x1 x2) = binunion (setminus x0 x1) (setminus x0 x2) (proof)
Theorem f0846..^{setminus_binunion} : ∀ x0 x1 x2 . setminus x0 (binunion x1 x2) = setminus (setminus x0 x1) x2 (proof)
Theorem e58ae..^{binintersect_setminus} : ∀ x0 x1 x2 . setminus (binintersect x0 x1) x2 = binintersect x0 (setminus x1 x2) (proof)
Theorem 1a1e7..^{binunion_setminus} : ∀ x0 x1 x2 . setminus (binunion x0 x1) x2 = binunion (setminus x0 x2) (setminus x1 x2) (proof)
Theorem 0253c..^{setminus_setminus} : ∀ x0 x1 x2 . setminus x0 (setminus x1 x2) = binunion (setminus x0 x1) (binintersect x0 x2) (proof)
Theorem 0227e..^{setminus_annil} : ∀ x0 . setminus 0 x0 = 0 (proof)
Known 3cfc3..^nIn_Empty : ∀ x0 . nIn x0 0
Theorem 5ff7d..^setminus_idr : ∀ x0 . setminus x0 0 = x0 (proof)
Theorem b4d92..^{tab_pos_setminus} : ∀ x0 x1 x2 . In x2 (setminus x0 x1) ⟶ (In x2 x0 ⟶ nIn x2 x1 ⟶ False) ⟶ False (proof)
Theorem 34f38..^{tab_neg_setminus} : ∀ x0 x1 x2 . nIn x2 (setminus x0 x1) ⟶ (nIn x2 x0 ⟶ False) ⟶ (In x2 x1 ⟶ False) ⟶ False (proof)