Theorem brrelex1i 5361

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

Syntax hints:   → wi 4   ∈ wcel 2157  Vcvv 3383   class class class wbr 4841  Rel wrel 5315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2375  ax-ext 2775  ax-sep 4973  ax-nul 4981  ax-pr 5095

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ral 3092  df-rex 3093  df-rab 3096  df-v 3385  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4114  df-if 4276  df-sn 4367  df-pr 4369  df-op 4373  df-br 4842  df-opab 4904  df-xp 5316  df-rel 5317

This theorem is referenced by:  nprrel  5364  vtoclr  5367  opeliunxp2  5462  ideqg  5475  issetid  5478  dffv2  6494  brfvopabrbr  6502  brrpssg  7171  opeliunxp2f  7572  brtpos2  7594  brdomg  8203  isfi  8217  en1uniel  8265  domdifsn  8283  undom  8288  xpdom2  8295  xpdom1g  8297  sbth  8320  dom0  8328  sdom0  8332  sdomirr  8337  sdomdif  8348  fodomr  8351  pwdom  8352  xpen  8363  pwen  8373  php3  8386  sucdom2  8396  sdom1  8400  fineqv  8415  f1finf1o  8427  infsdomnn  8461  relprcnfsupp  8518  fsuppimp  8521  fsuppunbi  8536  mapfien2  8554  harword  8710  brwdom  8712  domwdom  8719  brwdom3i  8728  unwdomg  8729  xpwdomg  8730  infdifsn  8802  ac10ct  9141  inffien  9170  iunfictbso  9221  cdaen  9281  cdadom1  9294  cdafi  9298  cdainflem  9299  cdalepw  9304  unctb  9313  infcdaabs  9314  infunabs  9315  infmap2  9326  cfslb2n  9376  fin4i  9406  isfin5  9407  isfin6  9408  fin4en1  9417  isfin4-3  9423  isfin32i  9473  fin45  9500  fin56  9501  fin67  9503  hsmexlem1  9534  hsmexlem3  9536  axcc3  9546  ttukeylem1  9617  brdom3  9636  iundom2g  9648  iundom  9650  iunctb  9682  gchi  9732  engch  9736  gchdomtri  9737  fpwwe2lem6  9743  fpwwe2lem7  9744  fpwwe2lem9  9746  gchpwdom  9778  prcdnq  10101  reexALT  12064  hasheni  13384  hashdomi  13415  brfi1indALT  13527  climcl  14567  climi  14578  climrlim2  14615  climrecl  14651  climge0  14652  iseralt  14752  climfsum  14886  structex  16191  issubc  16805  pmtrfv  18180  dprdval  18714  frgpcyg  20239  lindff  20475  lindfind  20476  f1lindf  20482  lindfmm  20487  lsslindf  20490  lbslcic  20501  1stcrestlem  21580  2ndcdisj2  21585  dis2ndc  21588  hauspwdom  21629  refbas  21638  refssex  21639  reftr  21642  refun0  21643  ovoliunnul  23611  uniiccdif  23682  dvle  24107  subgrv  26495  cyclnspth  27045  hlimi  28561  brsset  32500  brbigcup  32509  elfix2  32515  brcolinear2  32669  isfne  32837  refssfne  32856  ovoliunnfl  33931  voliunnfl  33933  volsupnfl  33934  brabg2  33989  heiborlem4  34091  isrngo  34174  isdivrngo  34227  brssr  34736  fphpd  38153  ctbnfien  38155  climd  40635  climuzlem  40706  rlimdmafv  42018  rlimdmafv2  42099  linindsv  43020