Theorem brrelexi 4029

Description: The first argument of a binary relation exists. (An artifact of our ordered pair definition.)

Hypothesis

Ref	Expression
brrelexi.1	|- Rel R

Assertion

Ref	Expression
brrelexi	|- (ARB -> A e. _V)

Proof of Theorem brrelexi

Step	Hyp	Ref	Expression
1		brrelexi.1	. 2 |- Rel R
2		brrelex 4028	. 2 |- ((Rel R /\ ARB) -> A e. _V)
3	1, 2	mpan 759	1 |- (ARB -> A e. _V)

Syntax hints:   -> wi 3   e. wcel 1300  _Vcvv 2292   class class class wbr 3338  Rel wrel 3991

This theorem is referenced by:  nprrel 4030  vtoclr 4032  vtoclrbr 4033  vtoclrbrOLD 4034  vtoclibr 4035  ideqg 4114  ideqgOLD 4115  issetid 4121  issetidOLD 4122  dffv2 4734  oprprc1 4908  breng 5434  brdomg 5435  isfi 5441  ensymg 5470  unen 5493  xpdom2 5501  xpdom1 5502  ac6sfi 5509  sbth 5520  domnsym 5526  ensdomtr 5534  sdomirr 5535  sdomex 5536  domsdomtr 5539  sdomen2 5545  fodomr 5547  pwen 5597  php3 5609  infsdomnn 5625  unifi 5648  fodomfi 5656  card1 5983  alephnbtwn2 6017  alephsucdom 6028  prcdpq 6249  climcl 8238  clmi1i 8346  climaddci 8392  climmulci 8393  climabslem 8408  unctb 8846  eltopsp 8873  tpsex 8874  ismsg 9077  isgalem 9449  isring 9465  fbssint 10279  fora 10408  isdivrng 10417  epelcNEW 13826  brsset 14069  brbigcup 14074  elfix2 14078  sndw 14428  istopgrp 14971  tarax3f 15229  isfne 15480  isref 15488  fnetr 15495  reftr 15497  refssfne 15504  islocfin 15506  brabg2 15681

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-br 3339  df-opab 3396  df-xp 4000  df-rel 4001

Copyright terms: Public domain