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

Metamath Proof Explorer

Theorem relopabiALT

Description: Alternate proof of relopabi (shorter but uses more axioms). (Contributed by Mario Carneiro, 21-Dec-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis relopabi.1 ⊢ 𝐴 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
Assertion relopabiALT Rel 𝐴

Proof

Step Hyp Ref Expression
1 relopabi.1 ⊢ 𝐴 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
2 df-opab ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
3 1 2 eqtri ⊢ 𝐴 = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
4 vex ⊢ 𝑥 ∈ V
5 vex ⊢ 𝑦 ∈ V
6 4 5 opelvv ⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V × V )
7 eleq1 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ ( V × V ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( V × V ) ) )
8 6 7 mpbiri ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 ∈ ( V × V ) )
9 8 adantr ⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → 𝑧 ∈ ( V × V ) )
10 9 exlimivv ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → 𝑧 ∈ ( V × V ) )
11 10 abssi ⊢ { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } ⊆ ( V × V )
12 3 11 eqsstri ⊢ 𝐴 ⊆ ( V × V )
13 df-rel ⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( V × V ) )
14 12 13 mpbir ⊢ Rel 𝐴