Theorem brrelex1i 5711

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3450   class class class wbr 5103  Rel wrel 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5661  df-rel 5662

This theorem is used by:  nprrel  5714  opeliunxp2  5818  ideqg  5831  issetid  5834  dffv2  6974  brfvopabrbr  6984  brrpssg  7727  opeliunxp2f  8209  brtpos2  8231  brdomg  8967  ctex  8972  isfi  8984  domssr  9008  domdifsn  9061  xpdom2  9073  xpdom1g  9075  sbth  9098  sdomirr  9115  sdomdif  9126  fodomr  9129  pwdom  9130  xpen  9141  pwen  9151  sbthfi  9196  sucdom2  9200  fineqv  9240  infsdomnn  9274  relprcnfsupp  9337  fsuppssov1  9357  fsuppunbi  9362  mapfien2  9382  harword  9538  brwdom  9542  domwdom  9549  brwdom3i  9558  unwdomg  9559  xpwdomg  9560  infdifsn  9639  ac10ct  10040  inffien  10069  djuen  10175  djudom2  10189  djufi  10192  cdainflem  10193  djulepw  10198  infdjuabs  10210  infunabs  10211  infmap2  10222  cfslb2n  10273  fin4i  10303  isfin5  10304  isfin6  10305  fin4en1  10314  isfin4p1  10320  isfin32i  10370  fin45  10397  fin56  10398  fin67  10400  hsmexlem1  10431  hsmexlem3  10433  axcc3  10443  ttukeylem1  10514  brdom3  10534  iundom2g  10551  iundom  10553  gchi  10636  engch  10640  gchdomtri  10641  fpwwe2lem5  10647  fpwwe2lem6  10648  fpwwe2lem8  10650  gchdjuidm  10680  gchpwdom  10682  prcdnq  11005  reexALT  13037  hasheni  14415  hashdomi  14447  climcl  15589  climi  15600  climrlim2  15637  climrecl  15673  climge0  15674  iseralt  15775  climfsum  15910  structex  17245  issubc  17927  pmtrfv  19582  dprdval  20135  frgpcyg  21789  lindff  22031  lindfind  22032  f1lindf  22038  lindfmm  22043  lsslindf  22046  lbslcic  22057  psrbaglesupp  22140  hauspwdom  23730  refbas  23739  refssex  23740  reftr  23743  refun0  23744  ovoliunnul  25738  dvle  26237  cyclnspth  30271  hlimi  31672  gsumhashmul  33510  extdgval  34166  finextfldext  34177  kardenir  35687  karddom  35690  kardsdom  35691  usgrgt2cycl  35726  brsset  36469  brbigcup  36478  elfix2  36484  brcolinear2  36641  isfne  36961  refssfne  36980  bj-epelg  37815  bj-ideqb  37914  bj-opelidb1ALT  37921  ovoliunnfl  38414  voliunnfl  38416  volsupnfl  38417  brabg2  38470  heiborlem4  38567  isrngo  38650  isdivrngo  38703  brssr  39332  issetssr  39334  fphpd  43660  ctbnfien  43662  sdomne0  44256  climd  46503  climuzlem  46574  rlimdmafv  48068  rlimdmafv2  48149  imasubc  50080  imassc  50082  imaid  50083  imaf1co  50084  imasubc3  50085  fuco112  50258  fuco111  50259  fuco21  50265  fucoid  50277