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 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }