Theorem en1bOLD

Description: Obsolete version of en1b as of 24-Sep-2024. (Contributed by Mario Carneiro, 17-Jan-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	en1bOLD	⊢ ( 𝐴 ≈ 1o ↔ 𝐴 = { ∪ 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		en1	⊢ ( 𝐴 ≈ 1o ↔ ∃ 𝑥 𝐴 = { 𝑥 } )
2		id	⊢ ( 𝐴 = { 𝑥 } → 𝐴 = { 𝑥 } )
3		unieq	⊢ ( 𝐴 = { 𝑥 } → ∪ 𝐴 = ∪ { 𝑥 } )
4		vex	⊢ 𝑥 ∈ V
5	4	unisn	⊢ ∪ { 𝑥 } = 𝑥
6	3 5	eqtrdi	⊢ ( 𝐴 = { 𝑥 } → ∪ 𝐴 = 𝑥 )
7	6	sneqd	⊢ ( 𝐴 = { 𝑥 } → { ∪ 𝐴 } = { 𝑥 } )
8	2 7	eqtr4d	⊢ ( 𝐴 = { 𝑥 } → 𝐴 = { ∪ 𝐴 } )
9	8	exlimiv	⊢ ( ∃ 𝑥 𝐴 = { 𝑥 } → 𝐴 = { ∪ 𝐴 } )
10	1 9	sylbi	⊢ ( 𝐴 ≈ 1o → 𝐴 = { ∪ 𝐴 } )
11		id	⊢ ( 𝐴 = { ∪ 𝐴 } → 𝐴 = { ∪ 𝐴 } )
12		snex	⊢ { ∪ 𝐴 } ∈ V
13	11 12	eqeltrdi	⊢ ( 𝐴 = { ∪ 𝐴 } → 𝐴 ∈ V )
14	13	uniexd	⊢ ( 𝐴 = { ∪ 𝐴 } → ∪ 𝐴 ∈ V )
15		ensn1g	⊢ ( ∪ 𝐴 ∈ V → { ∪ 𝐴 } ≈ 1o )
16	14 15	syl	⊢ ( 𝐴 = { ∪ 𝐴 } → { ∪ 𝐴 } ≈ 1o )
17	11 16	eqbrtrd	⊢ ( 𝐴 = { ∪ 𝐴 } → 𝐴 ≈ 1o )
18	10 17	impbii	⊢ ( 𝐴 ≈ 1o ↔ 𝐴 = { ∪ 𝐴 } )