Theorem brrelex12i 5678

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  Vcvv 3439   class class class wbr 5097  Rel wrel 5628

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 5240  ax-nul 5250  ax-pr 5376

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 3051  df-rex 3060  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-xp 5629  df-rel 5630

This theorem is referenced by:  nprrel12  5681  vtoclr  5686  relbrcnvg  6063  ovprc  7396  oprabv  7418  encv  8893  brdomi  8898  domssl  8937  fsuppimp  9273  fsuppunbi  9294  brttrcl  9624  brfi1uzind  14433  brfi1indALT  14435  isstruct2  17078  brssc  17740  isfull  17838  isfth  17842  dvdsr  20300  ulmval  26347  subgrv  29324  vcex  30634  opelco3  35948  bj-ideqgALT  37332  bj-idreseqb  37337  bj-ideqg1ALT  37339  rngoablo2  38079  aovprc  47471  aovrcl  47472  nelbrim  47558  linindsv  48728  func1st  49359  func2nd  49360  oppfval  49418  upfval3  49460  prcofval  49660