Description: The first argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by NM, 4-Jun-1998)
Ref | Expression | ||
---|---|---|---|
Hypothesis | brrelexi.1 | ⊢ Rel 𝑅 | |
Assertion | brrelex1i | ⊢ ( 𝐴 𝑅 𝐵 → 𝐴 ∈ V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brrelexi.1 | ⊢ Rel 𝑅 | |
2 | brrelex1 | ⊢ ( ( Rel 𝑅 ∧ 𝐴 𝑅 𝐵 ) → 𝐴 ∈ V ) | |
3 | 1 2 | mpan | ⊢ ( 𝐴 𝑅 𝐵 → 𝐴 ∈ V ) |