Theorem brrelex1i 5719

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Vcvv 3457   class class class wbr 5111  Rel wrel 5668

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-xp 5669  df-rel 5670

This theorem is used by:  nprrel  5722  opeliunxp2  5826  ideqg  5839  issetid  5842  dffv2  6980  brfvopabrbr  6990  brrpssg  7732  opeliunxp2f  8212  brtpos2  8234  brdomg  8961  ctex  8966  isfi  8978  domssr  9002  domdifsn  9055  xpdom2  9067  xpdom1g  9069  sbth  9092  sdomirr  9109  sdomdif  9120  fodomr  9123  pwdom  9124  xpen  9135  pwen  9145  sbthfi  9190  sucdom2  9194  fineqv  9234  infsdomnn  9268  relprcnfsupp  9331  fsuppssov1  9351  fsuppunbi  9356  mapfien2  9376  harword  9532  brwdom  9536  domwdom  9543  brwdom3i  9552  unwdomg  9553  xpwdomg  9554  infdifsn  9633  ac10ct  10034  inffien  10063  djuen  10169  djudom2  10183  djufi  10186  cdainflem  10187  djulepw  10192  infdjuabs  10204  infunabs  10205  infmap2  10216  cfslb2n  10267  fin4i  10297  isfin5  10298  isfin6  10299  fin4en1  10308  isfin4p1  10314  isfin32i  10364  fin45  10391  fin56  10392  fin67  10394  hsmexlem1  10425  hsmexlem3  10427  axcc3  10437  ttukeylem1  10508  brdom3  10528  iundom2g  10543  iundom  10545  gchi  10628  engch  10632  gchdomtri  10633  fpwwe2lem5  10639  fpwwe2lem6  10640  fpwwe2lem8  10642  gchdjuidm  10672  gchpwdom  10674  prcdnq  10997  reexALT  13028  hasheni  14406  hashdomi  14438  climcl  15578  climi  15589  climrlim2  15626  climrecl  15662  climge0  15663  iseralt  15764  climfsum  15899  structex  17236  issubc  17918  pmtrfv  19570  dprdval  20123  frgpcyg  21777  lindff  22019  lindfind  22020  f1lindf  22026  lindfmm  22031  lsslindf  22034  lbslcic  22045  psrbaglesupp  22126  hauspwdom  23713  refbas  23722  refssex  23723  reftr  23726  refun0  23727  ovoliunnul  25721  dvle  26221  cyclnspth  30220  hlimi  31615  gsumhashmul  33455  extdgval  34111  finextfldext  34122  kardenir  35632  karddom  35635  kardsdom  35636  usgrgt2cycl  35671  brsset  36420  brbigcup  36429  elfix2  36435  brcolinear2  36591  isfne  36911  refssfne  36930  bj-epelg  37765  bj-ideqb  37864  bj-opelidb1ALT  37871  ovoliunnfl  38374  voliunnfl  38376  volsupnfl  38377  brabg2  38430  heiborlem4  38527  isrngo  38610  isdivrngo  38663  brssr  39292  issetssr  39294  fphpd  43620  ctbnfien  43622  sdomne0  44216  climd  46463  climuzlem  46534  rlimdmafv  47991  rlimdmafv2  48072  imasubc  50005  imassc  50007  imaid  50008  imaf1co  50009  imasubc3  50010  fuco112  50183  fuco111  50184  fuco21  50190  fucoid  50202