Theorem brrelex2 5709

Description: If two classes are related by a binary relation, then the second class is a set. (Contributed by Mario Carneiro, 26-Apr-2015.)

Assertion

Ref	Expression
brrelex2	⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V)

Proof of Theorem brrelex2

Step	Hyp	Ref	Expression
1		brrelex12 5707	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2	1	simprd 501	1 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐵 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  Vcvv 3454   class class class wbr 5106  Rel wrel 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-xp 5661  df-rel 5662

This theorem is used by:  brrelex2i  5712  releldm  5931  relelrn  5932  elrelimasn  6090  funbrfv  6944  relbrtpos  8268  ertr  8747  erth  8786  fsuppss  9388  pslem  18761  opeldifid  33250  eqvreltr  39766  eqvrelth  39770  frege124d  44904  frege133d  44908  climfv  46843  funbrafv2  48459