Theorem brrelex12i 5705

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  Vcvv 3450   class class class wbr 5102  Rel wrel 5655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-xp 5656  df-rel 5657

This theorem is used by:  nprrel12  5708  vtoclr  5713  relbrcnvg  6100  ovprc  7458  oprabv  7480  encv  8981  brdomi  8986  domssl  9025  fsuppimp  9360  fsuppunbi  9381  brttrcl  9714  brfi1uzind  14653  brfi1indALT  14655  isstruct2  17327  brssc  17989  isfull  18087  isfth  18091  dvdsr  20592  ulmval  26707  subgrv  29851  vcex  31180  opelco3  36539  bj-ideqgALT  38080  bj-idreseqb  38085  bj-ideqg1ALT  38087  rngoablo2  38844  aovprc  48258  aovrcl  48259  nelbrim  48345  linindsv  49557  func1st  50185  func2nd  50186  oppfval  50244  upfval3  50286  prcofval  50486