Theorem brrelex12 5295

Description: A true binary relation on a relation implies the arguments are sets. (This is a property of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)

Assertion

Ref	Expression
brrelex12	⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))

Proof of Theorem brrelex12

Step	Hyp	Ref	Expression
1		df-rel 5256	. . . . 5 ⊢ (Rel 𝑅 ↔ 𝑅 ⊆ (V × V))
2	1	biimpi 206	. . . 4 ⊢ (Rel 𝑅 → 𝑅 ⊆ (V × V))
3	2	ssbrd 4827	. . 3 ⊢ (Rel 𝑅 → (𝐴𝑅𝐵 → 𝐴(V × V)𝐵))
4	3	imp 393	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴(V × V)𝐵)
5		brxp 5287	. 2 ⊢ (𝐴(V × V)𝐵 ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V))
6	4, 5	sylib 208	1 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))

Syntax hints:   → wi 4   ∧ wa 382   ∈ wcel 2144  Vcvv 3349   ⊆ wss 3721   class class class wbr 4784   × cxp 5247  Rel wrel 5254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pr 5034

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-br 4785  df-opab 4845  df-xp 5255  df-rel 5256

This theorem is referenced by:  brrelex  5296  brrelex2  5297  nprrel12  5300  relbrcnvg  5645  ovprc  6827  oprabv  6849  brovex  7499  ersym  7907  relelec  7938  encv  8116  fsuppunbi  8451  fpwwe2lem2  9655  fpwwelem  9668  brfi1uzind  13481  isstruct2  16073  brssc  16680  cofuval2  16753  isfull  16776  isfth  16780  isnat  16813  pslem  17413  frgpuplem  18391  dvdsr  18853  ulmval  24353  perpln1  25825  perpln2  25826  opelco3  32008  rngoablo2  34033  aovprc  41782  aovrcl  41783  nelbrim  41809