Metamath Proof Explorer


Theorem bropaex12

Description: Two classes related by an ordered-pair class abstraction 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 ) )