Theorem bropaex12

Description: Two classes related by an ordered pair class builder are sets. (Contributed by AV, 21-Jan-2020)

	Ref	Expression
Hypothesis	bropaex12.1	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 }
Assertion	bropaex12	⊢ ( 𝐴 𝑅 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		bropaex12.1	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 }
2		df-br	⊢ ( 𝐴 𝑅 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
3	1	eleq2i	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } )
4	2 3	bitri	⊢ ( 𝐴 𝑅 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } )
5		elopaelxp	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V ) )
6	4 5	sylbi	⊢ ( 𝐴 𝑅 𝐵 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V ) )
7		opelxp	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V ) ↔ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
8	6 7	sylib	⊢ ( 𝐴 𝑅 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )