This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elpreimad

Description: Membership in the preimage of a set under a function. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses elpreimad.f ⊢ φ → F Fn A
elpreimad.b ⊢ φ → B ∈ A
elpreimad.c ⊢ φ → F ⁡ B ∈ C
Assertion elpreimad ⊢ φ → B ∈ F -1 C

Proof

Step Hyp Ref Expression
1 elpreimad.f ⊢ φ → F Fn A
2 elpreimad.b ⊢ φ → B ∈ A
3 elpreimad.c ⊢ φ → F ⁡ B ∈ C
4 elpreima ⊢ F Fn A → B ∈ F -1 C ↔ B ∈ A ∧ F ⁡ B ∈ C
5 1 4 syl ⊢ φ → B ∈ F -1 C ↔ B ∈ A ∧ F ⁡ B ∈ C
6 2 3 5 mpbir2and ⊢ φ → B ∈ F -1 C