Metamath Proof Explorer


Theorem oprabrexex2

Description: Existence of an existentially restricted operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010)

Ref Expression
Hypotheses oprabrexex2.1 𝐴 ∈ V
oprabrexex2.2 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ∈ V
Assertion oprabrexex2 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑤𝐴 𝜑 } ∈ V

Proof

Step Hyp Ref Expression
1 oprabrexex2.1 𝐴 ∈ V
2 oprabrexex2.2 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ∈ V
3 df-oprab { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑤𝐴 𝜑 } = { 𝑣 ∣ ∃ 𝑥𝑦𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ∃ 𝑤𝐴 𝜑 ) }
4 rexcom4 ( ∃ 𝑤𝐴𝑥𝑦𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥𝑤𝐴𝑦𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
5 rexcom4 ( ∃ 𝑤𝐴𝑦𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑦𝑤𝐴𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
6 rexcom4 ( ∃ 𝑤𝐴𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑧𝑤𝐴 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
7 r19.42v ( ∃ 𝑤𝐴 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ∃ 𝑤𝐴 𝜑 ) )
8 7 exbii ( ∃ 𝑧𝑤𝐴 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ∃ 𝑤𝐴 𝜑 ) )
9 6 8 bitri ( ∃ 𝑤𝐴𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ∃ 𝑤𝐴 𝜑 ) )
10 9 exbii ( ∃ 𝑦𝑤𝐴𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑦𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ∃ 𝑤𝐴 𝜑 ) )
11 5 10 bitri ( ∃ 𝑤𝐴𝑦𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑦𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ∃ 𝑤𝐴 𝜑 ) )
12 11 exbii ( ∃ 𝑥𝑤𝐴𝑦𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥𝑦𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ∃ 𝑤𝐴 𝜑 ) )
13 4 12 bitr2i ( ∃ 𝑥𝑦𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ∃ 𝑤𝐴 𝜑 ) ↔ ∃ 𝑤𝐴𝑥𝑦𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
14 13 abbii { 𝑣 ∣ ∃ 𝑥𝑦𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ∃ 𝑤𝐴 𝜑 ) } = { 𝑣 ∣ ∃ 𝑤𝐴𝑥𝑦𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) }
15 3 14 eqtri { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑤𝐴 𝜑 } = { 𝑣 ∣ ∃ 𝑤𝐴𝑥𝑦𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) }
16 df-oprab { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { 𝑣 ∣ ∃ 𝑥𝑦𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) }
17 16 2 eqeltrri { 𝑣 ∣ ∃ 𝑥𝑦𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) } ∈ V
18 1 17 abrexex2 { 𝑣 ∣ ∃ 𝑤𝐴𝑥𝑦𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) } ∈ V
19 15 18 eqeltri { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑤𝐴 𝜑 } ∈ V