Theorem brrelex1i 5705

Description: The first argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by NM, 4-Jun-1998.)

Hypothesis

Ref	Expression
brrelexi.1	⊢ Rel 𝑅

Assertion

Ref	Expression
brrelex1i	⊢ (𝐴𝑅𝐵 → 𝐴 ∈ V)

Proof of Theorem brrelex1i

Step	Hyp	Ref	Expression
1		brrelexi.1	. 2 ⊢ Rel 𝑅
2		brrelex1 5702	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V)
3	1, 2	mpan 700	1 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2144  Vcvv 3456   class class class wbr 5102  Rel wrel 5654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-pr 5392

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103  df-opab 5165  df-xp 5655  df-rel 5656

This theorem is referenced by:  nprrel  5708  opeliunxp2  5812  ideqg  5825  issetid  5828  dffv2  6964  brfvopabrbr  6974  brrpssg  7710  opeliunxp2f  8192  brtpos2  8214  brdomg  8941  ctex  8946  isfi  8958  domssr  8982  domdifsn  9034  xpdom2  9046  xpdom1g  9048  sbth  9071  sdomirr  9088  sdomdif  9099  fodomr  9102  pwdom  9103  xpen  9114  pwen  9124  sbthfi  9169  sucdom2  9173  fineqv  9213  infsdomnn  9247  relprcnfsupp  9312  fsuppssov1  9332  fsuppunbi  9337  mapfien2  9357  harword  9513  brwdom  9517  domwdom  9524  brwdom3i  9533  unwdomg  9534  xpwdomg  9535  infdifsn  9614  ac10ct  9992  inffien  10021  djuen  10128  djudom2  10142  djufi  10145  cdainflem  10146  djulepw  10151  infdjuabs  10163  infunabs  10164  infmap2  10175  cfslb2n  10227  fin4i  10257  isfin5  10258  isfin6  10259  fin4en1  10268  isfin4p1  10274  isfin32i  10324  fin45  10351  fin56  10352  fin67  10354  hsmexlem1  10385  hsmexlem3  10387  axcc3  10397  ttukeylem1  10468  brdom3  10487  iundom2g  10499  iundom  10501  gchi  10584  engch  10588  gchdomtri  10589  fpwwe2lem5  10595  fpwwe2lem6  10596  fpwwe2lem8  10598  gchdjuidm  10628  gchpwdom  10630  prcdnq  10953  reexALT  12987  hasheni  14363  hashdomi  14395  climcl  15528  climi  15539  climrlim2  15576  climrecl  15612  climge0  15613  iseralt  15714  climfsum  15850  structex  17188  issubc  17870  pmtrfv  19494  dprdval  20047  frgpcyg  21627  lindff  21869  lindfind  21870  f1lindf  21876  lindfmm  21881  lsslindf  21884  lbslcic  21895  psrbaglesupp  21976  hauspwdom  23563  refbas  23572  refssex  23573  reftr  23576  refun0  23577  ovoliunnul  25571  dvle  26071  cyclnspth  30003  hlimi  31393  gsumhashmul  33249  extdgval  33952  finextfldext  33963  usgrgt2cycl  35485  brsset  36242  brbigcup  36251  elfix2  36257  brcolinear2  36413  isfne  36704  refssfne  36723  bj-epelg  37558  bj-ideqb  37656  bj-opelidb1ALT  37663  ovoliunnfl  38166  voliunnfl  38168  volsupnfl  38169  brabg2  38221  heiborlem4  38318  isrngo  38401  isdivrngo  38454  brssr  39085  issetssr  39087  fphpd  43398  ctbnfien  43400  sdomne0  43994  climd  46251  climuzlem  46322  rlimdmafv  47776  rlimdmafv2  47857  imasubc  49777  imassc  49779  imaid  49780  imaf1co  49781  imasubc3  49782  fuco112  49955  fuco111  49956  fuco21  49962  fucoid  49974