Metamath Proof Explorer

Theorem elmapintab

Description: Two ways to say a set is an element of mapped intersection of a class. Here F maps elements of C to elements of |^| { x | ph } or x . (Contributed by RP, 19-Aug-2020)

Ref Expression
Hypotheses elmapintab.1 ⊢ A ∈ B ↔ A ∈ C ∧ F ⁡ A ∈ ⋂ x | φ
elmapintab.2 ⊢ A ∈ E ↔ A ∈ C ∧ F ⁡ A ∈ x
Assertion elmapintab ⊢ A ∈ B ↔ A ∈ C ∧ ∀ x φ → A ∈ E

Proof

Step Hyp Ref Expression
1 elmapintab.1 ⊢ A ∈ B ↔ A ∈ C ∧ F ⁡ A ∈ ⋂ x | φ
2 elmapintab.2 ⊢ A ∈ E ↔ A ∈ C ∧ F ⁡ A ∈ x
3 fvex ⊢ F ⁡ A ∈ V
4 3 elintab ⊢ F ⁡ A ∈ ⋂ x | φ ↔ ∀ x φ → F ⁡ A ∈ x
5 4 anbi2i ⊢ A ∈ C ∧ F ⁡ A ∈ ⋂ x | φ ↔ A ∈ C ∧ ∀ x φ → F ⁡ A ∈ x
6 2 baibr ⊢ A ∈ C → F ⁡ A ∈ x ↔ A ∈ E
7 6 imbi2d ⊢ A ∈ C → φ → F ⁡ A ∈ x ↔ φ → A ∈ E
8 7 albidv ⊢ A ∈ C → ∀ x φ → F ⁡ A ∈ x ↔ ∀ x φ → A ∈ E
9 8 pm5.32i ⊢ A ∈ C ∧ ∀ x φ → F ⁡ A ∈ x ↔ A ∈ C ∧ ∀ x φ → A ∈ E
10 1 5 9 3bitri ⊢ A ∈ B ↔ A ∈ C ∧ ∀ x φ → A ∈ E