**Description:** If an ordered pair has an element, then its arguments are sets.
(Contributed by Mario Carneiro, 26-Apr-2015)

Ref | Expression | ||
---|---|---|---|

Assertion | oprcl | ⊢ ( 𝐶 ∈ ⟨ 𝐴 , 𝐵 ⟩ → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | n0i | ⊢ ( 𝐶 ∈ ⟨ 𝐴 , 𝐵 ⟩ → ¬ ⟨ 𝐴 , 𝐵 ⟩ = ∅ ) | |

2 | opprc | ⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ⟨ 𝐴 , 𝐵 ⟩ = ∅ ) | |

3 | 1 2 | nsyl2 | ⊢ ( 𝐶 ∈ ⟨ 𝐴 , 𝐵 ⟩ → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) |