Theorem brrelex12i 5676

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2121  Vcvv 3433   class class class wbr 5075  Rel wrel 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076  df-opab 5138  df-xp 5627  df-rel 5628

This theorem is referenced by:  nprrel12  5679  vtoclr  5684  relbrcnvg  6064  ovprc  7398  oprabv  7420  encv  8895  brdomi  8900  domssl  8939  fsuppimp  9275  fsuppunbi  9296  brttrcl  9629  brfi1uzind  14465  brfi1indALT  14467  isstruct2  17114  brssc  17776  isfull  17874  isfth  17878  dvdsr  20337  ulmval  26367  subgrv  29361  vcex  30671  opelco3  36018  bj-ideqgALT  37533  bj-idreseqb  37538  bj-ideqg1ALT  37540  rngoablo2  38291  aovprc  47665  aovrcl  47666  nelbrim  47752  linindsv  48950  func1st  49581  func2nd  49582  oppfval  49640  upfval3  49682  prcofval  49882