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 703	1 ⊢ (𝐴𝑅𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  Vcvv 3453   class class class wbr 5107  Rel wrel 5664

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-xp 5665  df-rel 5666

This theorem is used by:  nprrel12  5717  vtoclr  5722  relbrcnvg  6105  ovprc  7454  oprabv  7476  encv  8963  brdomi  8968  domssl  9007  fsuppimp  9341  fsuppunbi  9362  brttrcl  9695  brfi1uzind  14575  brfi1indALT  14577  isstruct2  17245  brssc  17907  isfull  18005  isfth  18009  dvdsr  20504  ulmval  26613  subgrv  29716  vcex  31045  opelco3  36341  bj-ideqgALT  37897  bj-idreseqb  37902  bj-ideqg1ALT  37904  rngoablo2  38646  aovprc  48063  aovrcl  48064  nelbrim  48150  linindsv  49362  func1st  49990  func2nd  49991  oppfval  50049  upfval3  50091  prcofval  50291