Theorem brrelex12i 5686

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Vcvv 3444   class class class wbr 5102  Rel wrel 5636

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 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-rel 5638

This theorem is referenced by:  nprrel12  5689  vtoclr  5694  relbrcnvg  6065  ovprc  7407  oprabv  7429  encv  8903  brdomi  8908  domssl  8946  fsuppimp  9295  fsuppunbi  9316  brttrcl  9642  brfi1uzind  14449  brfi1indALT  14451  isstruct2  17095  brssc  17756  isfull  17854  isfth  17858  dvdsr  20282  ulmval  26322  subgrv  29250  vcex  30557  opelco3  35755  bj-ideqgALT  37139  bj-idreseqb  37144  bj-ideqg1ALT  37146  rngoablo2  37896  aovprc  47182  aovrcl  47183  nelbrim  47269  linindsv  48427  func1st  49059  func2nd  49060  oppfval  49118  upfval3  49160  prcofval  49360