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 { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ∧ 𝜑 ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝜓 ) }