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	⊢ ( 𝐴 ∈ 𝐵 ↔ ( 𝐴 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝐴 ) ∈ ∩ { 𝑥 ∣ 𝜑 } ) )
	elmapintab.2	⊢ ( 𝐴 ∈ 𝐸 ↔ ( 𝐴 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 ) )
Assertion	elmapintab	⊢ ( 𝐴 ∈ 𝐵 ↔ ( 𝐴 ∈ 𝐶 ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝐸 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elmapintab.1	⊢ ( 𝐴 ∈ 𝐵 ↔ ( 𝐴 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝐴 ) ∈ ∩ { 𝑥 ∣ 𝜑 } ) )
2		elmapintab.2	⊢ ( 𝐴 ∈ 𝐸 ↔ ( 𝐴 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 ) )
3		fvex	⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
4	3	elintab	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ∩ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 ) )
5	4	anbi2i	⊢ ( ( 𝐴 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝐴 ) ∈ ∩ { 𝑥 ∣ 𝜑 } ) ↔ ( 𝐴 ∈ 𝐶 ∧ ∀ 𝑥 ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 ) ) )
6	2	baibr	⊢ ( 𝐴 ∈ 𝐶 → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 ↔ 𝐴 ∈ 𝐸 ) )
7	6	imbi2d	⊢ ( 𝐴 ∈ 𝐶 → ( ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 ) ↔ ( 𝜑 → 𝐴 ∈ 𝐸 ) ) )
8	7	albidv	⊢ ( 𝐴 ∈ 𝐶 → ( ∀ 𝑥 ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 ) ↔ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝐸 ) ) )
9	8	pm5.32i	⊢ ( ( 𝐴 ∈ 𝐶 ∧ ∀ 𝑥 ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ 𝑥 ) ) ↔ ( 𝐴 ∈ 𝐶 ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝐸 ) ) )
10	1 5 9	3bitri	⊢ ( 𝐴 ∈ 𝐵 ↔ ( 𝐴 ∈ 𝐶 ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝐸 ) ) )