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

Theorem brrelexi 5313
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
brrelexi (𝐴𝑅𝐵𝐴 ∈ V)

Proof of Theorem brrelexi
StepHypRef Expression
1 brrelexi.1 . 2 Rel 𝑅
2 brrelex 5311 . 2 ((Rel 𝑅𝐴𝑅𝐵) → 𝐴 ∈ V)
31, 2mpan 708 1 (𝐴𝑅𝐵𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2137  Vcvv 3338   class class class wbr 4802  Rel wrel 5269
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pr 5053
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ral 3053  df-rex 3054  df-rab 3057  df-v 3340  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-sn 4320  df-pr 4322  df-op 4326  df-br 4803  df-opab 4863  df-xp 5270  df-rel 5271
This theorem is referenced by:  nprrel  5316  vtoclr  5319  opeliunxp2  5414  ideqg  5427  issetid  5430  dffv2  6431  brfvopabrbr  6439  brrpssg  7102  opeliunxp2f  7503  brtpos2  7525  brdomg  8129  isfi  8143  en1uniel  8191  domdifsn  8206  undom  8211  xpdom2  8218  xpdom1g  8220  sbth  8243  dom0  8251  sdom0  8255  sdomirr  8260  sdomdif  8271  fodomr  8274  pwdom  8275  xpen  8286  pwen  8296  php3  8309  sucdom2  8319  sdom1  8323  fineqv  8338  f1finf1o  8350  infsdomnn  8384  relprcnfsupp  8441  fsuppimp  8444  fsuppunbi  8459  mapfien2  8477  harword  8633  brwdom  8635  domwdom  8642  brwdom3i  8651  unwdomg  8652  xpwdomg  8653  infdifsn  8725  ac10ct  9045  inffien  9074  iunfictbso  9125  cdaen  9185  cdadom1  9198  cdafi  9202  cdainflem  9203  cdalepw  9208  unctb  9217  infcdaabs  9218  infunabs  9219  infmap2  9230  cfslb2n  9280  fin4i  9310  isfin5  9311  isfin6  9312  fin4en1  9321  isfin4-3  9327  isfin32i  9377  fin45  9404  fin56  9405  fin67  9407  hsmexlem1  9438  hsmexlem3  9440  axcc3  9450  ttukeylem1  9521  brdom3  9540  iundom2g  9552  iundom  9554  iunctb  9586  gchi  9636  engch  9640  gchdomtri  9641  fpwwe2lem6  9647  fpwwe2lem7  9648  fpwwe2lem9  9650  gchpwdom  9682  prcdnq  10005  reexALT  12017  hasheni  13328  hashdomi  13359  brfi1indALT  13472  climcl  14427  climi  14438  climrlim2  14475  climrecl  14511  climge0  14512  iseralt  14612  climfsum  14749  structex  16068  issubc  16694  pmtrfv  18070  dprdval  18600  frgpcyg  20122  lindff  20354  lindfind  20355  f1lindf  20361  lindfmm  20366  lsslindf  20369  lbslcic  20380  1stcrestlem  21455  2ndcdisj2  21460  dis2ndc  21463  hauspwdom  21504  refbas  21513  refssex  21514  reftr  21517  refun0  21518  ovoliunnul  23473  uniiccdif  23544  dvle  23967  subgrv  26359  cyclnspth  26904  hlimi  28352  brsset  32300  brbigcup  32309  elfix2  32315  brcolinear2  32469  isfne  32638  refssfne  32657  ovoliunnfl  33762  voliunnfl  33764  volsupnfl  33765  brabg2  33821  heiborlem4  33924  isrngo  34007  isdivrngo  34060  brssr  34572  fphpd  37880  ctbnfien  37882  climd  40405  climuzlem  40476  rlimdmafv  41761  linindsv  42742
  Copyright terms: Public domain W3C validator