Theorem brrelex12i 5715

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∈ wcel 2142  Vcvv 3454   class class class wbr 5108  Rel wrel 5665

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256  ax-pr 5403

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-opab 5173  df-xp 5666  df-rel 5667

This theorem is used by:  nprrel12  5718  vtoclr  5723  relbrcnvg  6106  ovprc  7450  oprabv  7472  encv  8949  brdomi  8954  domssl  8993  fsuppimp  9326  fsuppunbi  9347  brttrcl  9680  brfi1uzind  14552  brfi1indALT  14554  isstruct2  17215  brssc  17877  isfull  17975  isfth  17979  dvdsr  20451  ulmval  26554  subgrv  29631  vcex  30941  opelco3  36275  bj-ideqgALT  37830  bj-idreseqb  37835  bj-ideqg1ALT  37837  rngoablo2  38588  aovprc  47953  aovrcl  47954  nelbrim  48040  linindsv  49253  func1st  49883  func2nd  49884  oppfval  49942  upfval3  49984  prcofval  50184