Theorem brrelex2i 5698

Description: The second argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)

Hypothesis

Ref	Expression
brrelexi.1	⊢ Rel 𝑅

Assertion

Ref	Expression
brrelex2i	⊢ (𝐴𝑅𝐵 → 𝐵 ∈ V)

Proof of Theorem brrelex2i

Step	Hyp	Ref	Expression
1		brrelexi.1	. 2 ⊢ Rel 𝑅
2		brrelex2 5695	. 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:  vtoclr  5704  brfvopabrbr  6968  domdifsn  9028  undom  9033  undomOLD  9034  xpdom2  9041  xpdom1g  9043  domunsncan  9046  enfixsn  9055  sucdom2OLD  9056  fodomr  9098  pwdom  9099  domssex  9108  xpen  9110  mapdom1  9112  mapdom2  9118  pwen  9120  domtrfil  9162  sucdom2  9173  0sdom1dom  9192  1sdom2dom  9201  unxpdom  9207  unxpdom2  9208  sucxpdom  9209  isfinite2  9252  infn0ALT  9259  fin2inf  9260  fodomfir  9286  suppeqfsuppbi  9337  fsuppsssupp  9339  fsuppssov1  9342  fsuppunbi  9347  funsnfsupp  9350  mapfien2  9367  wemapso2  9513  card2on  9514  elharval  9521  harword  9523  brwdomi  9528  brwdomn0  9529  domwdom  9534  wdomtr  9535  wdompwdom  9538  canthwdom  9539  brwdom3i  9543  unwdomg  9544  xpwdomg  9545  unxpwdom  9549  infdifsn  9617  infdiffi  9618  isnum2  9905  wdomfil  10021  djuen  10130  djuenun  10131  djudom2  10144  djuxpdom  10146  djuinf  10149  infdju1  10150  pwdjuidm  10152  djulepw  10153  infdjuabs  10165  infdif  10168  pwdjudom  10175  infpss  10176  infmap2  10177  fictb  10204  infpssALT  10273  enfin2i  10281  fin34  10350  fodomb  10486  wdomac  10487  iundom2g  10500  iundom  10502  sdomsdomcard  10520  infxpidm  10522  engch  10588  fpwwe2lem3  10593  canthp1lem1  10612  canthp1lem2  10613  canthp1  10614  pwfseq  10624  pwxpndom2  10625  pwxpndom  10626  pwdjundom  10627  hargch  10633  gchaclem  10638  hasheni  14320  hashdomi  14352  clim  15467  rlim  15468  ntrivcvgn0  15871  ssc1  17790  ssc2  17791  ssctr  17794  frgpnabl  19812  dprddomprc  19939  dprdval  19942  dprdgrp  19944  dprdf  19945  dprdssv  19955  subgdmdprd  19973  dprd2da  19981  1stcrestlem  23346  hauspwdom  23395  isref  23403  ufilen  23824  dvle  25919  ellpi  33351  locfinref  33838  isfne4  36335  fnetr  36346  topfneec  36350  fnessref  36352  refssfne  36353  bj-epelb  37064  bj-idreseq  37157  phpreu  37605  sdomne0  43409  sdomne0d  43410  rn1st  45274  climf  45627  climf2  45671  iinfssc  49050  fuco21  49329  fucoid  49341