Theorem brrelex1i 5687

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3444   class class class wbr 5102  Rel wrel 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-rel 5638

This theorem is referenced by:  nprrel  5690  opeliunxp2  5792  ideqg  5805  issetid  5808  dffv2  6938  brfvopabrbr  6947  brrpssg  7681  opeliunxp2f  8166  brtpos2  8188  brdomg  8907  ctex  8912  isfi  8924  domssr  8947  domdifsn  9001  xpdom2  9013  xpdom1g  9015  sbth  9038  sdomirr  9055  sdomdif  9066  fodomr  9069  pwdom  9070  xpen  9081  pwen  9091  sbthfi  9140  sucdom2  9144  fineqv  9186  f1finf1oOLD  9193  infsdomnn  9225  infsdomnnOLD  9226  relprcnfsupp  9291  fsuppssov1  9311  fsuppunbi  9316  mapfien2  9336  harword  9492  brwdom  9496  domwdom  9503  brwdom3i  9512  unwdomg  9513  xpwdomg  9514  infdifsn  9586  ac10ct  9963  inffien  9992  djuen  10099  djudom2  10113  djufi  10116  cdainflem  10117  djulepw  10122  infdjuabs  10134  infunabs  10135  infmap2  10146  cfslb2n  10197  fin4i  10227  isfin5  10228  isfin6  10229  fin4en1  10238  isfin4p1  10244  isfin32i  10294  fin45  10321  fin56  10322  fin67  10324  hsmexlem1  10355  hsmexlem3  10357  axcc3  10367  ttukeylem1  10438  brdom3  10457  iundom2g  10469  iundom  10471  gchi  10553  engch  10557  gchdomtri  10558  fpwwe2lem5  10564  fpwwe2lem6  10565  fpwwe2lem8  10567  gchdjuidm  10597  gchpwdom  10599  prcdnq  10922  reexALT  12919  hasheni  14289  hashdomi  14321  climcl  15441  climi  15452  climrlim2  15489  climrecl  15525  climge0  15526  iseralt  15627  climfsum  15762  structex  17096  issubc  17777  pmtrfv  19366  dprdval  19919  frgpcyg  21515  lindff  21757  lindfind  21758  f1lindf  21764  lindfmm  21769  lsslindf  21772  lbslcic  21783  psrbaglesupp  21864  hauspwdom  23421  refbas  23430  refssex  23431  reftr  23434  refun0  23435  ovoliunnul  25441  dvle  25945  cyclnspth  29781  hlimi  31167  gsumhashmul  33044  extdgval  33642  usgrgt2cycl  35110  brsset  35870  brbigcup  35879  elfix2  35885  brcolinear2  36039  isfne  36320  refssfne  36339  bj-epelg  37049  bj-ideqb  37140  bj-opelidb1ALT  37147  ovoliunnfl  37649  voliunnfl  37651  volsupnfl  37652  brabg2  37704  heiborlem4  37801  isrngo  37884  isdivrngo  37937  brssr  38485  issetssr  38487  fphpd  42797  ctbnfien  42799  sdomne0  43395  climd  45663  climuzlem  45734  rlimdmafv  47171  rlimdmafv2  47252  imasubc  49133  imassc  49135  imaid  49136  imaf1co  49137  imasubc3  49138  fuco112  49311  fuco111  49312  fuco21  49318  fucoid  49330