MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  brrelex1i Structured version   Visualization version   GIF version

Theorem brrelex1i 5607
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
StepHypRef Expression
1 brrelexi.1 . 2 Rel 𝑅
2 brrelex1 5604 . 2 ((Rel 𝑅𝐴𝑅𝐵) → 𝐴 ∈ V)
31, 2mpan 686 1 (𝐴𝑅𝐵𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  Vcvv 3500   class class class wbr 5063  Rel wrel 5559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pr 5326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-br 5064  df-opab 5126  df-xp 5560  df-rel 5561
This theorem is referenced by:  nprrel  5610  opeliunxp2  5708  ideqg  5721  issetid  5724  dffv2  6753  brfvopabrbr  6762  brrpssg  7441  opeliunxp2f  7867  brtpos2  7889  brdomg  8508  ctex  8513  isfi  8522  en1uniel  8570  domdifsn  8589  undom  8594  xpdom2  8601  xpdom1g  8603  sbth  8626  dom0  8634  sdom0  8638  sdomirr  8643  sdomdif  8654  fodomr  8657  pwdom  8658  xpen  8669  pwen  8679  php3  8692  sucdom2  8703  sdom1  8707  fineqv  8722  f1finf1o  8734  infsdomnn  8768  relprcnfsupp  8825  fsuppunbi  8843  mapfien2  8861  harword  9018  brwdom  9020  domwdom  9027  brwdom3i  9036  unwdomg  9037  xpwdomg  9038  infdifsn  9109  ac10ct  9449  inffien  9478  djuen  9584  djudom2  9598  djufi  9601  cdainflem  9602  djulepw  9607  infdjuabs  9617  infunabs  9618  infmap2  9629  cfslb2n  9679  fin4i  9709  isfin5  9710  isfin6  9711  fin4en1  9720  isfin4p1  9726  isfin32i  9776  fin45  9803  fin56  9804  fin67  9806  hsmexlem1  9837  hsmexlem3  9839  axcc3  9849  ttukeylem1  9920  brdom3  9939  iundom2g  9951  iundom  9953  gchi  10035  engch  10039  gchdomtri  10040  fpwwe2lem6  10046  fpwwe2lem7  10047  fpwwe2lem9  10049  gchdjuidm  10079  gchpwdom  10081  prcdnq  10404  reexALT  12373  hasheni  13698  hashdomi  13731  brfi1indALT  13848  climcl  14846  climi  14857  climrlim2  14894  climrecl  14930  climge0  14931  iseralt  15031  climfsum  15165  structex  16484  issubc  17095  pmtrfv  18500  dprdval  19045  frgpcyg  20636  lindff  20875  lindfind  20876  f1lindf  20882  lindfmm  20887  lsslindf  20890  lbslcic  20901  hauspwdom  22025  refbas  22034  refssex  22035  reftr  22038  refun0  22039  ovoliunnul  24023  dvle  24519  cyclnspth  27495  hlimi  28879  extdgval  30930  usgrgt2cycl  32261  brsset  33234  brbigcup  33243  elfix2  33249  brcolinear2  33403  isfne  33571  refssfne  33590  bj-epelg  34241  bj-ideqb  34330  bj-opelidb1ALT  34337  ovoliunnfl  34801  voliunnfl  34803  volsupnfl  34804  brabg2  34859  heiborlem4  34960  isrngo  35043  isdivrngo  35096  brssr  35608  issetssr  35610  fphpd  39278  ctbnfien  39280  climd  41818  climuzlem  41889  rlimdmafv  43242  rlimdmafv2  43323
  Copyright terms: Public domain W3C validator