Theorem brrelex12i 5593

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2110  Vcvv 3401   class class class wbr 5043  Rel wrel 5545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2706  ax-sep 5181  ax-nul 5188  ax-pr 5311

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2713  df-cleq 2726  df-clel 2812  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3403  df-dif 3860  df-un 3862  df-in 3864  df-ss 3874  df-nul 4228  df-if 4430  df-sn 4532  df-pr 4534  df-op 4538  df-br 5044  df-opab 5106  df-xp 5546  df-rel 5547

This theorem is referenced by:  nprrel12  5596  vtoclr  5601  relbrcnvg  5962  ovprc  7240  oprabv  7260  encv  8623  fsuppimp  8980  fsuppunbi  8995  brfi1uzind  14047  brfi1indALT  14049  isstruct2  16694  brssc  17291  isfull  17389  isfth  17393  dvdsr  19636  ulmval  25244  subgrv  27330  vcex  28631  opelco3  33437  bj-ideqgALT  35021  bj-idreseqb  35026  bj-ideqg1ALT  35028  rngoablo2  35761  aovprc  44306  aovrcl  44307  nelbrim  44393  isisomgr  44903  linindsv  45413