This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Power Sets Functions fniniseg
Description: Membership in the preimage of a singleton, under a function. (Contributed by Mario Carneiro , 12-May-2014) (Proof shortened by Mario Carneiro , 28-Apr-2015)
Ref
Expression
Assertion
fniniseg ⊢ ( 𝐹 Fn 𝐴 → ( 𝐶 ∈ ( ◡ 𝐹 “ { 𝐵 } ) ↔ ( 𝐶 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝐶 ) = 𝐵 ) ) )
Proof
Step
Hyp
Ref
Expression
1
elpreima ⊢ ( 𝐹 Fn 𝐴 → ( 𝐶 ∈ ( ◡ 𝐹 “ { 𝐵 } ) ↔ ( 𝐶 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝐶 ) ∈ { 𝐵 } ) ) )
2
fvex ⊢ ( 𝐹 ‘ 𝐶 ) ∈ V
3
2
elsn ⊢ ( ( 𝐹 ‘ 𝐶 ) ∈ { 𝐵 } ↔ ( 𝐹 ‘ 𝐶 ) = 𝐵 )
4
3
anbi2i ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝐶 ) ∈ { 𝐵 } ) ↔ ( 𝐶 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝐶 ) = 𝐵 ) )
5
1 4
bitrdi ⊢ ( 𝐹 Fn 𝐴 → ( 𝐶 ∈ ( ◡ 𝐹 “ { 𝐵 } ) ↔ ( 𝐶 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝐶 ) = 𝐵 ) ) )