| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dfclel 2816 | . 2
⊢ (𝐴 ∈ sngl 𝐵 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ sngl 𝐵)) | 
| 2 |  | df-bj-sngl 36968 | . . . . 5
⊢ sngl
𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = {𝑥}} | 
| 3 | 2 | eqabri 2884 | . . . 4
⊢ (𝑦 ∈ sngl 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑦 = {𝑥}) | 
| 4 | 3 | anbi2i 623 | . . 3
⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ sngl 𝐵) ↔ (𝑦 = 𝐴 ∧ ∃𝑥 ∈ 𝐵 𝑦 = {𝑥})) | 
| 5 | 4 | exbii 1847 | . 2
⊢
(∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ sngl 𝐵) ↔ ∃𝑦(𝑦 = 𝐴 ∧ ∃𝑥 ∈ 𝐵 𝑦 = {𝑥})) | 
| 6 |  | r19.42v 3190 | . . . . 5
⊢
(∃𝑥 ∈
𝐵 (𝑦 = 𝐴 ∧ 𝑦 = {𝑥}) ↔ (𝑦 = 𝐴 ∧ ∃𝑥 ∈ 𝐵 𝑦 = {𝑥})) | 
| 7 | 6 | bicomi 224 | . . . 4
⊢ ((𝑦 = 𝐴 ∧ ∃𝑥 ∈ 𝐵 𝑦 = {𝑥}) ↔ ∃𝑥 ∈ 𝐵 (𝑦 = 𝐴 ∧ 𝑦 = {𝑥})) | 
| 8 | 7 | exbii 1847 | . . 3
⊢
(∃𝑦(𝑦 = 𝐴 ∧ ∃𝑥 ∈ 𝐵 𝑦 = {𝑥}) ↔ ∃𝑦∃𝑥 ∈ 𝐵 (𝑦 = 𝐴 ∧ 𝑦 = {𝑥})) | 
| 9 |  | rexcom4 3287 | . . . 4
⊢
(∃𝑥 ∈
𝐵 ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 = {𝑥}) ↔ ∃𝑦∃𝑥 ∈ 𝐵 (𝑦 = 𝐴 ∧ 𝑦 = {𝑥})) | 
| 10 | 9 | bicomi 224 | . . 3
⊢
(∃𝑦∃𝑥 ∈ 𝐵 (𝑦 = 𝐴 ∧ 𝑦 = {𝑥}) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 = {𝑥})) | 
| 11 |  | eqcom 2743 | . . . . . 6
⊢ (𝐴 = {𝑥} ↔ {𝑥} = 𝐴) | 
| 12 |  | vsnex 5433 | . . . . . . 7
⊢ {𝑥} ∈ V | 
| 13 | 12 | eqvinc 3648 | . . . . . 6
⊢ ({𝑥} = 𝐴 ↔ ∃𝑦(𝑦 = {𝑥} ∧ 𝑦 = 𝐴)) | 
| 14 |  | exancom 1860 | . . . . . 6
⊢
(∃𝑦(𝑦 = {𝑥} ∧ 𝑦 = 𝐴) ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 = {𝑥})) | 
| 15 | 11, 13, 14 | 3bitri 297 | . . . . 5
⊢ (𝐴 = {𝑥} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 = {𝑥})) | 
| 16 | 15 | bicomi 224 | . . . 4
⊢
(∃𝑦(𝑦 = 𝐴 ∧ 𝑦 = {𝑥}) ↔ 𝐴 = {𝑥}) | 
| 17 | 16 | rexbii 3093 | . . 3
⊢
(∃𝑥 ∈
𝐵 ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 = {𝑥}) ↔ ∃𝑥 ∈ 𝐵 𝐴 = {𝑥}) | 
| 18 | 8, 10, 17 | 3bitri 297 | . 2
⊢
(∃𝑦(𝑦 = 𝐴 ∧ ∃𝑥 ∈ 𝐵 𝑦 = {𝑥}) ↔ ∃𝑥 ∈ 𝐵 𝐴 = {𝑥}) | 
| 19 | 1, 5, 18 | 3bitri 297 | 1
⊢ (𝐴 ∈ sngl 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 = {𝑥}) |