Theorem brrelex1i 5756

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3488   class class class wbr 5166  Rel wrel 5705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-rel 5707

This theorem is referenced by:  nprrel  5759  opeliunxp2  5863  ideqg  5876  issetid  5879  dffv2  7017  brfvopabrbr  7026  brrpssg  7760  opeliunxp2f  8251  brtpos2  8273  brdomg  9016  brdomgOLD  9017  ctex  9023  isfi  9036  domssr  9059  en1unielOLD  9094  domdifsn  9120  undomOLD  9126  xpdom2  9133  xpdom1g  9135  sucdom2OLD  9148  sbth  9159  dom0OLD  9169  sdom0OLD  9175  sdomirr  9180  sdomdif  9191  fodomr  9194  pwdom  9195  xpen  9206  pwen  9216  sbthfi  9265  sucdom2  9269  php3OLD  9287  sdom1OLD  9306  fineqv  9326  f1finf1oOLD  9334  infsdomnn  9366  infsdomnnOLD  9367  relprcnfsupp  9434  fsuppssov1  9453  fsuppunbi  9458  mapfien2  9478  harword  9632  brwdom  9636  domwdom  9643  brwdom3i  9652  unwdomg  9653  xpwdomg  9654  infdifsn  9726  ac10ct  10103  inffien  10132  djuen  10239  djudom2  10253  djufi  10256  cdainflem  10257  djulepw  10262  infdjuabs  10274  infunabs  10275  infmap2  10286  cfslb2n  10337  fin4i  10367  isfin5  10368  isfin6  10369  fin4en1  10378  isfin4p1  10384  isfin32i  10434  fin45  10461  fin56  10462  fin67  10464  hsmexlem1  10495  hsmexlem3  10497  axcc3  10507  ttukeylem1  10578  brdom3  10597  iundom2g  10609  iundom  10611  gchi  10693  engch  10697  gchdomtri  10698  fpwwe2lem5  10704  fpwwe2lem6  10705  fpwwe2lem8  10707  gchdjuidm  10737  gchpwdom  10739  prcdnq  11062  reexALT  13049  hasheni  14397  hashdomi  14429  climcl  15545  climi  15556  climrlim2  15593  climrecl  15629  climge0  15630  iseralt  15733  climfsum  15868  structex  17197  issubc  17899  pmtrfv  19494  dprdval  20047  frgpcyg  21615  lindff  21858  lindfind  21859  f1lindf  21865  lindfmm  21870  lsslindf  21873  lbslcic  21884  psrbaglesupp  21965  hauspwdom  23530  refbas  23539  refssex  23540  reftr  23543  refun0  23544  ovoliunnul  25561  dvle  26066  cyclnspth  29836  hlimi  31220  gsumhashmul  33040  extdgval  33667  usgrgt2cycl  35098  brsset  35853  brbigcup  35862  elfix2  35868  brcolinear2  36022  isfne  36305  refssfne  36324  bj-epelg  37034  bj-ideqb  37125  bj-opelidb1ALT  37132  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  brabg2  37677  heiborlem4  37774  isrngo  37857  isdivrngo  37910  brssr  38457  issetssr  38459  fphpd  42772  ctbnfien  42774  sdomne0  43375  climd  45593  climuzlem  45664  rlimdmafv  47092  rlimdmafv2  47173