Theorem brrelex1i 5718

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

Syntax hints:   → wi 4   ∈ wcel 2149  Vcvv 3463   class class class wbr 5113  Rel wrel 5667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-xp 5668  df-rel 5669

This theorem is referenced by:  nprrel  5721  opeliunxp2  5825  ideqg  5838  issetid  5841  dffv2  6977  brfvopabrbr  6987  brrpssg  7723  opeliunxp2f  8206  brtpos2  8228  brdomg  8955  ctex  8960  isfi  8972  domssr  8996  domdifsn  9048  xpdom2  9060  xpdom1g  9062  sbth  9085  sdomirr  9102  sdomdif  9113  fodomr  9116  pwdom  9117  xpen  9128  pwen  9138  sbthfi  9183  sucdom2  9187  fineqv  9227  infsdomnn  9261  relprcnfsupp  9324  fsuppssov1  9344  fsuppunbi  9349  mapfien2  9369  harword  9525  brwdom  9529  domwdom  9536  brwdom3i  9545  unwdomg  9546  xpwdomg  9547  infdifsn  9626  ac10ct  10018  inffien  10047  djuen  10153  djudom2  10167  djufi  10170  cdainflem  10171  djulepw  10176  infdjuabs  10188  infunabs  10189  infmap2  10200  cfslb2n  10252  fin4i  10282  isfin5  10283  isfin6  10284  fin4en1  10293  isfin4p1  10299  isfin32i  10349  fin45  10376  fin56  10377  fin67  10379  hsmexlem1  10410  hsmexlem3  10412  axcc3  10422  ttukeylem1  10493  brdom3  10512  iundom2g  10524  iundom  10526  gchi  10609  engch  10613  gchdomtri  10614  fpwwe2lem5  10620  fpwwe2lem6  10621  fpwwe2lem8  10623  gchdjuidm  10653  gchpwdom  10655  prcdnq  10978  reexALT  13008  hasheni  14384  hashdomi  14416  climcl  15550  climi  15561  climrlim2  15598  climrecl  15634  climge0  15635  iseralt  15736  climfsum  15872  structex  17210  issubc  17892  pmtrfv  19522  dprdval  20075  frgpcyg  21692  lindff  21934  lindfind  21935  f1lindf  21941  lindfmm  21946  lsslindf  21949  lbslcic  21960  psrbaglesupp  22041  hauspwdom  23627  refbas  23636  refssex  23637  reftr  23640  refun0  23641  ovoliunnul  25635  dvle  26135  cyclnspth  30091  hlimi  31481  gsumhashmul  33328  extdgval  33988  finextfldext  33999  kardenir  35504  karddom  35507  kardsdom  35508  usgrgt2cycl  35555  brsset  36312  brbigcup  36321  elfix2  36327  brcolinear2  36483  isfne  36773  refssfne  36792  bj-epelg  37626  bj-ideqb  37725  bj-opelidb1ALT  37732  ovoliunnfl  38235  voliunnfl  38237  volsupnfl  38238  brabg2  38290  heiborlem4  38387  isrngo  38470  isdivrngo  38523  brssr  39154  issetssr  39156  fphpd  43469  ctbnfien  43471  sdomne0  44065  climd  46312  climuzlem  46383  rlimdmafv  47837  rlimdmafv2  47918  imasubc  49848  imassc  49850  imaid  49851  imaf1co  49852  imasubc3  49853  fuco112  50026  fuco111  50027  fuco21  50033  fucoid  50045