Theorem brrelex12i 5695

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Vcvv 3450   class class class wbr 5109  Rel wrel 5645

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 2702  ax-sep 5253  ax-nul 5263  ax-pr 5389

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-br 5110  df-opab 5172  df-xp 5646  df-rel 5647

This theorem is referenced by:  nprrel12  5698  vtoclr  5703  relbrcnvg  6078  ovprc  7427  oprabv  7451  encv  8928  brdomi  8933  domssl  8971  fsuppimp  9325  fsuppunbi  9346  brttrcl  9672  brfi1uzind  14479  brfi1indALT  14481  isstruct2  17125  brssc  17782  isfull  17880  isfth  17884  dvdsr  20277  ulmval  26295  subgrv  29203  vcex  30513  opelco3  35757  bj-ideqgALT  37141  bj-idreseqb  37146  bj-ideqg1ALT  37148  rngoablo2  37898  aovprc  47179  aovrcl  47180  nelbrim  47266  linindsv  48424  func1st  49056  func2nd  49057  oppfval  49115  upfval3  49157  prcofval  49357