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

Metamath Proof Explorer

Theorem dfoprab4

Description: Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 3-Sep-2007) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypothesis dfoprab4.1 ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ 𝜓 ) )
Assertion dfoprab4 { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜑 ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) }

Proof

Step Hyp Ref Expression
1 dfoprab4.1 ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ 𝜓 ) )
2 xpss ⊢ ( 𝐴 × 𝐵 ) ⊆ ( V × V )
3 2 sseli ⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) → 𝑤 ∈ ( V × V ) )
4 3 adantr ⊢ ( ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜑 ) → 𝑤 ∈ ( V × V ) )
5 4 pm4.71ri ⊢ ( ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜑 ) ↔ ( 𝑤 ∈ ( V × V ) ∧ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜑 ) ) )
6 5 opabbii ⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜑 ) } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( V × V ) ∧ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜑 ) ) }
7 eleq1 ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) )
8 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
9 7 8 bitrdi ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
10 9 1 anbi12d ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) ) )
11 10 dfoprab3 ⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( V × V ) ∧ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜑 ) ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) }
12 6 11 eqtri ⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜑 ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) }