Theorem brrelex12i 5638

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  Vcvv 3430   class class class wbr 5074  Rel wrel 5590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5222  ax-nul 5229  ax-pr 5351

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3432  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5075  df-opab 5137  df-xp 5591  df-rel 5592

This theorem is referenced by:  nprrel12  5641  vtoclr  5646  relbrcnvg  6007  ovprc  7306  oprabv  7326  encv  8729  brdomi  8736  fsuppimp  9122  fsuppunbi  9137  brttrcl  9459  brfi1uzind  14200  brfi1indALT  14202  isstruct2  16838  brssc  17514  isfull  17614  isfth  17618  dvdsr  19876  ulmval  25527  subgrv  27625  vcex  28926  opelco3  33735  bj-ideqgALT  35315  bj-idreseqb  35320  bj-ideqg1ALT  35322  rngoablo2  36053  aovprc  44636  aovrcl  44637  nelbrim  44723  isisomgr  45232  linindsv  45742