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

Metamath Proof Explorer

Theorem brabv

Description: If two classes are in a relationship given by an ordered-pair class abstraction, the classes are sets. (Contributed by Alexander van der Vekens, 5-Nov-2017)

		Ref	Expression
	Assertion	brabv	⊢ ( 𝑋 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑌 → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		df-br	⊢ ( 𝑋 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑌 ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
2		opprc	⊢ ( ¬ ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ⟨ 𝑋 , 𝑌 ⟩ = ∅ )
3		0nelopab	⊢ ¬ ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
4		eleq1	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ = ∅ → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) )
5	3 4	mtbiri	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ = ∅ → ¬ ⟨ 𝑋 , 𝑌 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
6	2 5	syl	⊢ ( ¬ ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ¬ ⟨ 𝑋 , 𝑌 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
7	6	con4i	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
8	1 7	sylbi	⊢ ( 𝑋 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑌 → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )