Theorem brrelex12i 5714

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Vcvv 3464   class class class wbr 5124  Rel wrel 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-xp 5665  df-rel 5666

This theorem is referenced by:  nprrel12  5717  vtoclr  5722  relbrcnvg  6097  ovprc  7448  oprabv  7472  encv  8972  brdomi  8978  domssl  9017  fsuppimp  9385  fsuppunbi  9406  brttrcl  9732  brfi1uzind  14531  brfi1indALT  14533  isstruct2  17173  brssc  17832  isfull  17930  isfth  17934  dvdsr  20327  ulmval  26346  subgrv  29254  vcex  30564  opelco3  35797  bj-ideqgALT  37181  bj-idreseqb  37186  bj-ideqg1ALT  37188  rngoablo2  37938  aovprc  47184  aovrcl  47185  nelbrim  47271  linindsv  48388  oppfval  49049  upfval3  49080  prcofval  49256