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 𝐴