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

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