Theorem brrelex1i 5573

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

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3397   class class class wbr 5027  Rel wrel 5524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pr 5293

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-rex 3059  df-v 3399  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-sn 4514  df-pr 4516  df-op 4520  df-br 5028  df-opab 5090  df-xp 5525  df-rel 5526

This theorem is referenced by:  nprrel  5576  opeliunxp2  5675  ideqg  5688  issetid  5691  dffv2  6757  brfvopabrbr  6766  brrpssg  7463  opeliunxp2f  7898  brtpos2  7920  brdomg  8558  ctex  8563  isfi  8572  en1uniel  8621  domdifsn  8642  undom  8647  xpdom2  8654  xpdom1g  8656  sucdom2  8669  sbth  8680  dom0  8688  sdom0  8692  sdomirr  8697  sdomdif  8708  fodomr  8711  pwdom  8712  xpen  8723  pwen  8733  php3  8746  sdom1  8790  fineqv  8805  f1finf1o  8816  infsdomnn  8846  relprcnfsupp  8902  fsuppunbi  8920  mapfien2  8939  harword  9093  brwdom  9097  domwdom  9104  brwdom3i  9113  unwdomg  9114  xpwdomg  9115  infdifsn  9186  ac10ct  9527  inffien  9556  djuen  9662  djudom2  9676  djufi  9679  cdainflem  9680  djulepw  9685  infdjuabs  9699  infunabs  9700  infmap2  9711  cfslb2n  9761  fin4i  9791  isfin5  9792  isfin6  9793  fin4en1  9802  isfin4p1  9808  isfin32i  9858  fin45  9885  fin56  9886  fin67  9888  hsmexlem1  9919  hsmexlem3  9921  axcc3  9931  ttukeylem1  10002  brdom3  10021  iundom2g  10033  iundom  10035  gchi  10117  engch  10121  gchdomtri  10122  fpwwe2lem5  10128  fpwwe2lem6  10129  fpwwe2lem8  10131  gchdjuidm  10161  gchpwdom  10163  prcdnq  10486  reexALT  12459  hasheni  13793  hashdomi  13826  climcl  14939  climi  14950  climrlim2  14987  climrecl  15023  climge0  15024  iseralt  15127  climfsum  15261  structex  16590  issubc  17203  pmtrfv  18691  dprdval  19237  frgpcyg  20385  lindff  20624  lindfind  20625  f1lindf  20631  lindfmm  20636  lsslindf  20639  lbslcic  20650  psrbaglesupp  20730  hauspwdom  22245  refbas  22254  refssex  22255  reftr  22258  refun0  22259  ovoliunnul  24252  dvle  24751  cyclnspth  27733  hlimi  29115  gsumhashmul  30885  extdgval  31293  usgrgt2cycl  32655  brsset  33821  brbigcup  33830  elfix2  33836  brcolinear2  33990  isfne  34158  refssfne  34177  bj-epelg  34850  bj-ideqb  34940  bj-opelidb1ALT  34947  ovoliunnfl  35431  voliunnfl  35433  volsupnfl  35434  brabg2  35486  heiborlem4  35584  isrngo  35667  isdivrngo  35720  brssr  36231  issetssr  36233  fphpd  40194  ctbnfien  40196  climd  42739  climuzlem  42810  rlimdmafv  44186  rlimdmafv2  44267