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 2146  Vcvv 3454   class class class wbr 5106  Rel wrel 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-xp 5661  df-rel 5662

This theorem is used by:  nprrel  5714  opeliunxp2  5820  ideqg  5834  issetid  5837  dffv2  6991  brfvopabrbr  7001  brrpssg  7751  opeliunxp2f  8241  brtpos2  8263  brdomg  8999  ctex  9004  isfi  9016  domssr  9040  domdifsn  9093  xpdom2  9105  xpdom1g  9107  sbth  9130  sdomirr  9147  sdomdif  9158  fodomr  9161  pwdom  9162  xpen  9173  pwen  9183  sbthfi  9228  sucdom2  9232  fineqv  9272  infsdomnn  9307  relprcnfsupp  9370  fsuppssov1  9389  fsuppunbi  9394  mapfien2  9414  harword  9570  brwdom  9574  domwdom  9581  brwdom3i  9590  unwdomg  9591  xpwdomg  9592  infdifsn  9671  ac10ct  10126  inffien  10155  djuen  10261  djudom2  10275  djufi  10278  cdainflem  10279  djulepw  10284  infdjuabs  10296  infunabs  10297  infmap2  10308  cfslb2n  10359  fin4i  10389  isfin5  10390  isfin6  10391  fin4en1  10400  isfin4p1  10406  isfin32i  10456  fin45  10483  fin56  10484  fin67  10486  hsmexlem1  10517  hsmexlem3  10519  axcc3  10529  ttukeylem1  10600  brdom3  10620  iundom2g  10637  iundom  10639  gchi  10722  engch  10726  gchdomtri  10727  fpwwe2lem5  10733  fpwwe2lem6  10734  fpwwe2lem8  10736  gchdjuidm  10766  gchpwdom  10768  prcdnq  11091  reexALT  13125  hasheni  14505  hashdomi  14537  climcl  15681  climi  15692  climrlim2  15729  climrecl  15765  climge0  15766  iseralt  15867  climfsum  16002  structex  17343  issubc  18025  pmtrfv  19681  dprdval  20234  frgpcyg  21894  lindff  22136  lindfind  22137  f1lindf  22143  lindfmm  22148  lsslindf  22151  lbslcic  22162  psrbaglesupp  22245  hauspwdom  23835  refbas  23844  refssex  23845  reftr  23848  refun0  23849  ovoliunnul  25843  dvle  26342  cyclnspth  30404  hlimi  31805  gsumhashmul  33684  extdgval  34341  finextfldext  34352  kardenir  35900  karddom  35903  kardsdom  35904  usgrgt2cycl  36023  brsset  36784  brbigcup  36793  elfix2  36799  brcolinear2  36956  isfne  37260  refssfne  37279  bj-epelg  38128  bj-ideqb  38226  bj-opelidb1ALT  38233  ovoliunnfl  38726  voliunnfl  38728  volsupnfl  38729  brabg2  38797  heiborlem4  38894  isrngo  38977  isdivrngo  39030  brssr  39659  issetssr  39661  fphpd  43969  ctbnfien  43971  sdomne0  44560  climd  46827  climuzlem  46898  rlimdmafv  48392  rlimdmafv2  48473  imasubc  50412  imassc  50414  imaid  50415  imaf1co  50416  imasubc3  50417  fuco112  50596  fuco111  50597  fuco21  50603  fucoid  50615