Theorem phplem1OLD

Description: Obsolete lemma for php . (Contributed by NM, 25-May-1998) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	phplem1OLD	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = ( suc 𝐴 ∖ { 𝐵 } ) )

Proof

Step	Hyp	Ref	Expression
1		nnord	⊢ ( 𝐴 ∈ ω → Ord 𝐴 )
2		nordeq	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ) → 𝐴 ≠ 𝐵 )
3		disjsn2	⊢ ( 𝐴 ≠ 𝐵 → ( { 𝐴 } ∩ { 𝐵 } ) = ∅ )
4	2 3	syl	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( { 𝐴 } ∩ { 𝐵 } ) = ∅ )
5	1 4	sylan	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → ( { 𝐴 } ∩ { 𝐵 } ) = ∅ )
6		undif4	⊢ ( ( { 𝐴 } ∩ { 𝐵 } ) = ∅ → ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( { 𝐴 } ∪ 𝐴 ) ∖ { 𝐵 } ) )
7		df-suc	⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
8	7	equncomi	⊢ suc 𝐴 = ( { 𝐴 } ∪ 𝐴 )
9	8	difeq1i	⊢ ( suc 𝐴 ∖ { 𝐵 } ) = ( ( { 𝐴 } ∪ 𝐴 ) ∖ { 𝐵 } )
10	6 9	eqtr4di	⊢ ( ( { 𝐴 } ∩ { 𝐵 } ) = ∅ → ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = ( suc 𝐴 ∖ { 𝐵 } ) )
11	5 10	syl	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = ( suc 𝐴 ∖ { 𝐵 } ) )