Theorem brrelex12i 5704

Description: Two classes that are related by a binary relation are sets. Inference form. (Contributed by BJ, 3-Oct-2022.)

Hypothesis

Ref	Expression
brrelexi.1	⊢ Rel 𝑅

Assertion

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

Proof of Theorem brrelex12i

Step	Hyp	Ref	Expression
1		brrelexi.1	. 2 ⊢ Rel 𝑅
2		brrelex12 5701	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
3	1, 2	mpan 700	1 ⊢ (𝐴𝑅𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2144  Vcvv 3456   class class class wbr 5102  Rel wrel 5654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-pr 5392

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103  df-opab 5165  df-xp 5655  df-rel 5656

This theorem is referenced by:  nprrel12  5707  vtoclr  5712  relbrcnvg  6096  ovprc  7436  oprabv  7458  encv  8937  brdomi  8942  domssl  8981  fsuppimp  9316  fsuppunbi  9337  brttrcl  9670  brfi1uzind  14523  brfi1indALT  14525  isstruct2  17187  brssc  17849  isfull  17947  isfth  17951  dvdsr  20413  ulmval  26445  subgrv  29473  vcex  30783  opelco3  36130  bj-ideqgALT  37655  bj-idreseqb  37660  bj-ideqg1ALT  37662  rngoablo2  38413  aovprc  47787  aovrcl  47788  nelbrim  47874  linindsv  49072  func1st  49703  func2nd  49704  oppfval  49762  upfval3  49804  prcofval  50004