Metamath Proof Explorer

Theorem bj-elsngl

Description: Characterization of the elements of the singletonization of a class. (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion bj-elsngl ⊢A∈snglB↔∃x∈BA=x

Proof

Step Hyp Ref Expression
1 dfclel ⊢A∈snglB↔∃yy=A∧y∈snglB
2 df-bj-sngl ⊢snglB=y|∃x∈By=x
3 2 eqabri ⊢y∈snglB↔∃x∈By=x
4 3 anbi2i ⊢y=A∧y∈snglB↔y=A∧∃x∈By=x
5 4 exbii ⊢∃yy=A∧y∈snglB↔∃yy=A∧∃x∈By=x
6 r19.42v ⊢∃x∈By=A∧y=x↔y=A∧∃x∈By=x
7 6 bicomi ⊢y=A∧∃x∈By=x↔∃x∈By=A∧y=x
8 7 exbii ⊢∃yy=A∧∃x∈By=x↔∃y∃x∈By=A∧y=x
9 rexcom4 ⊢∃x∈B∃yy=A∧y=x↔∃y∃x∈By=A∧y=x
10 9 bicomi ⊢∃y∃x∈By=A∧y=x↔∃x∈B∃yy=A∧y=x
11 eqcom ⊢A=x↔x=A
12 vsnex ⊢x∈V
13 12 eqvinc ⊢x=A↔∃yy=x∧y=A
14 exancom ⊢∃yy=x∧y=A↔∃yy=A∧y=x
15 11 13 14 3bitri ⊢A=x↔∃yy=A∧y=x
16 15 bicomi ⊢∃yy=A∧y=x↔A=x
17 16 rexbii ⊢∃x∈B∃yy=A∧y=x↔∃x∈BA=x
18 8 10 17 3bitri ⊢∃yy=A∧∃x∈By=x↔∃x∈BA=x
19 1 5 18 3bitri ⊢A∈snglB↔∃x∈BA=x