Theorem brrelex1i 5697

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450   class class class wbr 5110  Rel wrel 5646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-rel 5648

This theorem is referenced by:  nprrel  5700  opeliunxp2  5805  ideqg  5818  issetid  5821  dffv2  6959  brfvopabrbr  6968  brrpssg  7704  opeliunxp2f  8192  brtpos2  8214  brdomg  8933  ctex  8938  isfi  8950  domssr  8973  domdifsn  9028  undomOLD  9034  xpdom2  9041  xpdom1g  9043  sucdom2OLD  9056  sbth  9067  sdomirr  9084  sdomdif  9095  fodomr  9098  pwdom  9099  xpen  9110  pwen  9120  sbthfi  9169  sucdom2  9173  sdom1OLD  9197  fineqv  9217  f1finf1oOLD  9224  infsdomnn  9256  infsdomnnOLD  9257  relprcnfsupp  9322  fsuppssov1  9342  fsuppunbi  9347  mapfien2  9367  harword  9523  brwdom  9527  domwdom  9534  brwdom3i  9543  unwdomg  9544  xpwdomg  9545  infdifsn  9617  ac10ct  9994  inffien  10023  djuen  10130  djudom2  10144  djufi  10147  cdainflem  10148  djulepw  10153  infdjuabs  10165  infunabs  10166  infmap2  10177  cfslb2n  10228  fin4i  10258  isfin5  10259  isfin6  10260  fin4en1  10269  isfin4p1  10275  isfin32i  10325  fin45  10352  fin56  10353  fin67  10355  hsmexlem1  10386  hsmexlem3  10388  axcc3  10398  ttukeylem1  10469  brdom3  10488  iundom2g  10500  iundom  10502  gchi  10584  engch  10588  gchdomtri  10589  fpwwe2lem5  10595  fpwwe2lem6  10596  fpwwe2lem8  10598  gchdjuidm  10628  gchpwdom  10630  prcdnq  10953  reexALT  12950  hasheni  14320  hashdomi  14352  climcl  15472  climi  15483  climrlim2  15520  climrecl  15556  climge0  15557  iseralt  15658  climfsum  15793  structex  17127  issubc  17804  pmtrfv  19389  dprdval  19942  frgpcyg  21490  lindff  21731  lindfind  21732  f1lindf  21738  lindfmm  21743  lsslindf  21746  lbslcic  21757  psrbaglesupp  21838  hauspwdom  23395  refbas  23404  refssex  23405  reftr  23408  refun0  23409  ovoliunnul  25415  dvle  25919  cyclnspth  29738  hlimi  31124  gsumhashmul  33008  extdgval  33656  usgrgt2cycl  35124  brsset  35884  brbigcup  35893  elfix2  35899  brcolinear2  36053  isfne  36334  refssfne  36353  bj-epelg  37063  bj-ideqb  37154  bj-opelidb1ALT  37161  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  brabg2  37718  heiborlem4  37815  isrngo  37898  isdivrngo  37951  brssr  38499  issetssr  38501  fphpd  42811  ctbnfien  42813  sdomne0  43409  climd  45677  climuzlem  45748  rlimdmafv  47182  rlimdmafv2  47263  imasubc  49144  imassc  49146  imaid  49147  imaf1co  49148  imasubc3  49149  fuco112  49322  fuco111  49323  fuco21  49329  fucoid  49341