Theorem brrelex1i 5694

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3447   class class class wbr 5107  Rel wrel 5643

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-rel 5645

This theorem is referenced by:  nprrel  5697  opeliunxp2  5802  ideqg  5815  issetid  5818  dffv2  6956  brfvopabrbr  6965  brrpssg  7701  opeliunxp2f  8189  brtpos2  8211  brdomg  8930  ctex  8935  isfi  8947  domssr  8970  domdifsn  9024  xpdom2  9036  xpdom1g  9038  sbth  9061  sdomirr  9078  sdomdif  9089  fodomr  9092  pwdom  9093  xpen  9104  pwen  9114  sbthfi  9163  sucdom2  9167  sdom1OLD  9190  fineqv  9210  f1finf1oOLD  9217  infsdomnn  9249  infsdomnnOLD  9250  relprcnfsupp  9315  fsuppssov1  9335  fsuppunbi  9340  mapfien2  9360  harword  9516  brwdom  9520  domwdom  9527  brwdom3i  9536  unwdomg  9537  xpwdomg  9538  infdifsn  9610  ac10ct  9987  inffien  10016  djuen  10123  djudom2  10137  djufi  10140  cdainflem  10141  djulepw  10146  infdjuabs  10158  infunabs  10159  infmap2  10170  cfslb2n  10221  fin4i  10251  isfin5  10252  isfin6  10253  fin4en1  10262  isfin4p1  10268  isfin32i  10318  fin45  10345  fin56  10346  fin67  10348  hsmexlem1  10379  hsmexlem3  10381  axcc3  10391  ttukeylem1  10462  brdom3  10481  iundom2g  10493  iundom  10495  gchi  10577  engch  10581  gchdomtri  10582  fpwwe2lem5  10588  fpwwe2lem6  10589  fpwwe2lem8  10591  gchdjuidm  10621  gchpwdom  10623  prcdnq  10946  reexALT  12943  hasheni  14313  hashdomi  14345  climcl  15465  climi  15476  climrlim2  15513  climrecl  15549  climge0  15550  iseralt  15651  climfsum  15786  structex  17120  issubc  17797  pmtrfv  19382  dprdval  19935  frgpcyg  21483  lindff  21724  lindfind  21725  f1lindf  21731  lindfmm  21736  lsslindf  21739  lbslcic  21750  psrbaglesupp  21831  hauspwdom  23388  refbas  23397  refssex  23398  reftr  23401  refun0  23402  ovoliunnul  25408  dvle  25912  cyclnspth  29731  hlimi  31117  gsumhashmul  33001  extdgval  33649  usgrgt2cycl  35117  brsset  35877  brbigcup  35886  elfix2  35892  brcolinear2  36046  isfne  36327  refssfne  36346  bj-epelg  37056  bj-ideqb  37147  bj-opelidb1ALT  37154  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  brabg2  37711  heiborlem4  37808  isrngo  37891  isdivrngo  37944  brssr  38492  issetssr  38494  fphpd  42804  ctbnfien  42806  sdomne0  43402  climd  45670  climuzlem  45741  rlimdmafv  47178  rlimdmafv2  47259  imasubc  49140  imassc  49142  imaid  49143  imaf1co  49144  imasubc3  49145  fuco112  49318  fuco111  49319  fuco21  49325  fucoid  49337