Theorem brrelex1i 5681

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3441   class class class wbr 5099  Rel wrel 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-xp 5631  df-rel 5632

This theorem is referenced by:  nprrel  5684  opeliunxp2  5788  ideqg  5801  issetid  5804  dffv2  6930  brfvopabrbr  6939  brrpssg  7672  opeliunxp2f  8154  brtpos2  8176  brdomg  8899  ctex  8904  isfi  8916  domssr  8940  domdifsn  8992  xpdom2  9004  xpdom1g  9006  sbth  9029  sdomirr  9046  sdomdif  9057  fodomr  9060  pwdom  9061  xpen  9072  pwen  9082  sbthfi  9127  sucdom2  9131  fineqv  9171  infsdomnn  9205  relprcnfsupp  9271  fsuppssov1  9291  fsuppunbi  9296  mapfien2  9316  harword  9472  brwdom  9476  domwdom  9483  brwdom3i  9492  unwdomg  9493  xpwdomg  9494  infdifsn  9570  ac10ct  9948  inffien  9977  djuen  10084  djudom2  10098  djufi  10101  cdainflem  10102  djulepw  10107  infdjuabs  10119  infunabs  10120  infmap2  10131  cfslb2n  10182  fin4i  10212  isfin5  10213  isfin6  10214  fin4en1  10223  isfin4p1  10229  isfin32i  10279  fin45  10306  fin56  10307  fin67  10309  hsmexlem1  10340  hsmexlem3  10342  axcc3  10352  ttukeylem1  10423  brdom3  10442  iundom2g  10454  iundom  10456  gchi  10539  engch  10543  gchdomtri  10544  fpwwe2lem5  10550  fpwwe2lem6  10551  fpwwe2lem8  10553  gchdjuidm  10583  gchpwdom  10585  prcdnq  10908  reexALT  12901  hasheni  14275  hashdomi  14307  climcl  15426  climi  15437  climrlim2  15474  climrecl  15510  climge0  15511  iseralt  15612  climfsum  15747  structex  17081  issubc  17763  pmtrfv  19385  dprdval  19938  frgpcyg  21532  lindff  21774  lindfind  21775  f1lindf  21781  lindfmm  21786  lsslindf  21789  lbslcic  21800  psrbaglesupp  21882  hauspwdom  23449  refbas  23458  refssex  23459  reftr  23462  refun0  23463  ovoliunnul  25468  dvle  25972  cyclnspth  29878  hlimi  31267  gsumhashmul  33152  extdgval  33812  finextfldext  33823  usgrgt2cycl  35326  brsset  36083  brbigcup  36092  elfix2  36098  brcolinear2  36254  isfne  36535  refssfne  36554  bj-epelg  37271  bj-ideqb  37366  bj-opelidb1ALT  37373  ovoliunnfl  37865  voliunnfl  37867  volsupnfl  37868  brabg2  37920  heiborlem4  38017  isrngo  38100  isdivrngo  38153  brssr  38784  issetssr  38786  fphpd  43125  ctbnfien  43127  sdomne0  43721  climd  45983  climuzlem  46054  rlimdmafv  47490  rlimdmafv2  47571  imasubc  49463  imassc  49465  imaid  49466  imaf1co  49467  imasubc3  49468  fuco112  49641  fuco111  49642  fuco21  49648  fucoid  49660