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 ) ) |
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 ) ) |