Theorem brrelex12i 5717

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  Vcvv 3461   class class class wbr 5111  Rel wrel 5667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5259  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-br 5112  df-opab 5176  df-xp 5668  df-rel 5669

This theorem is referenced by:  nprrel12  5720  vtoclr  5725  relbrcnvg  6108  ovprc  7449  oprabv  7471  encv  8951  brdomi  8956  domssl  8995  fsuppimp  9328  fsuppunbi  9349  brttrcl  9682  brfi1uzind  14545  brfi1indALT  14547  isstruct2  17209  brssc  17871  isfull  17969  isfth  17973  dvdsr  20444  ulmval  26509  subgrv  29561  vcex  30871  opelco3  36200  bj-ideqgALT  37725  bj-idreseqb  37730  bj-ideqg1ALT  37732  rngoablo2  38483  aovprc  47849  aovrcl  47850  nelbrim  47936  linindsv  49145  func1st  49775  func2nd  49776  oppfval  49834  upfval3  49876  prcofval  50076