Metamath Proof Explorer

Theorem dfoprab2

Description: Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by NM, 12-Mar-1995)

Ref Expression
Assertion dfoprab2 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }

Proof

Step Hyp Ref Expression
1 excom ⊢ ( ∃ 𝑧 ∃ 𝑤 ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ↔ ∃ 𝑤 ∃ 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
2 exrot4 ⊢ ( ∃ 𝑧 ∃ 𝑤 ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
3 opeq1 ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ⟨ 𝑤 , 𝑧 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
4 3 eqeq2d ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ↔ 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
5 4 pm5.32ri ⊢ ( ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) )
6 5 anbi1i ⊢ ( ( ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ 𝜑 ) ↔ ( ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ 𝜑 ) )
7 anass ⊢ ( ( ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ 𝜑 ) ↔ ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
8 an32 ⊢ ( ( ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ 𝜑 ) ↔ ( ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ∧ 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) )
9 6 7 8 3bitr3i ⊢ ( ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ↔ ( ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ∧ 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) )
10 9 exbii ⊢ ( ∃ 𝑤 ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ↔ ∃ 𝑤 ( ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ∧ 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) )
11 opex ⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
12 11 isseti ⊢ ∃ 𝑤 𝑤 = ⟨ 𝑥 , 𝑦 ⟩
13 19.42v ⊢ ( ∃ 𝑤 ( ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ∧ 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ∧ ∃ 𝑤 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) )
14 12 13 mpbiran2 ⊢ ( ∃ 𝑤 ( ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ∧ 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
15 10 14 bitri ⊢ ( ∃ 𝑤 ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ↔ ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
16 15 3exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
17 2 16 bitri ⊢ ( ∃ 𝑧 ∃ 𝑤 ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
18 19.42vv ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ↔ ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
19 18 2exbii ⊢ ( ∃ 𝑤 ∃ 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ↔ ∃ 𝑤 ∃ 𝑧 ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
20 1 17 19 3bitr3i ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑤 ∃ 𝑧 ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
21 20 abbii ⊢ { 𝑣 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) } = { 𝑣 ∣ ∃ 𝑤 ∃ 𝑧 ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) }
22 df-oprab ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { 𝑣 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) }
23 df-opab ⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } = { 𝑣 ∣ ∃ 𝑤 ∃ 𝑧 ( 𝑣 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) }
24 21 22 23 3eqtr4i ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }