Theorem brrelex12i 5675

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 5672	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
3	1, 2	mpan 691	1 ⊢ (𝐴𝑅𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  Vcvv 3427   class class class wbr 5074  Rel wrel 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-sep 5220  ax-pr 5364

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-br 5075  df-opab 5137  df-xp 5626  df-rel 5627

This theorem is referenced by:  nprrel12  5678  vtoclr  5683  relbrcnvg  6059  ovprc  7394  oprabv  7416  encv  8890  brdomi  8895  domssl  8934  fsuppimp  9270  fsuppunbi  9291  brttrcl  9623  brfi1uzind  14459  brfi1indALT  14461  isstruct2  17108  brssc  17770  isfull  17868  isfth  17872  dvdsr  20331  ulmval  26333  subgrv  29327  vcex  30637  opelco3  35945  bj-ideqgALT  37460  bj-idreseqb  37465  bj-ideqg1ALT  37467  rngoablo2  38218  aovprc  47624  aovrcl  47625  nelbrim  47711  linindsv  48909  func1st  49540  func2nd  49541  oppfval  49599  upfval3  49641  prcofval  49841