Theorem nfbr 5113

Description: Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)

Hypotheses

Ref	Expression
nfbr.1	⊢ Ⅎ𝑥𝐴
nfbr.2	⊢ Ⅎ𝑥𝑅
nfbr.3	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfbr	⊢ Ⅎ𝑥 𝐴𝑅𝐵

Proof of Theorem nfbr

Step	Hyp	Ref	Expression
1		nfbr.1	. . . 4 ⊢ Ⅎ𝑥𝐴
2	1	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
3		nfbr.2	. . . 4 ⊢ Ⅎ𝑥𝑅
4	3	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝑅)
5		nfbr.3	. . . 4 ⊢ Ⅎ𝑥𝐵
6	5	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐵)
7	2, 4, 6	nfbrd 5112	. 2 ⊢ (⊤ → Ⅎ𝑥 𝐴𝑅𝐵)
8	7	mptru 1544	1 ⊢ Ⅎ𝑥 𝐴𝑅𝐵

Syntax hints:  ⊤wtru 1538  Ⅎwnf 1784  Ⅎwnfc 2961   class class class wbr 5066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067

This theorem is referenced by:  sbcbr123  5120  nfpo  5479  nfso  5480  pofun  5491  nffr  5529  nfse  5530  nfco  5736  nfcnv  5749  dfdmf  5765  dfrnf  5820  nfdm  5823  dfrel4  6048  dffun6f  6369  nffv  6680  funfv2f  6752  fvopab5  6800  f1ompt  6875  fmptco  6891  nfiso  7075  nfofr  7415  ofrfval2  7427  tposoprab  7928  xpcomco  8607  nfoi  8978  tskwe  9379  cardmin2  9427  uniimadomf  9967  cardmin  9986  inar1  10197  lble  11593  rlim2  14853  ello1mpt  14878  rlimcld2  14935  o1compt  14944  nfsum1  15046  nfsumw  15047  nfsum  15048  fsum00  15153  fsumrlim  15166  o1fsum  15168  nfcprod1  15264  nfcprod  15265  sumeven  15738  sumodd  15739  invfuc  17244  dprd2d2  19166  2ndcdisj  22064  ovoliunlem3  24105  mbfpos  24252  mbfposb  24254  mbfsup  24265  mbfinf  24266  i1fposd  24308  itg2splitlem  24349  itg2split  24350  isibl2  24367  nfitg  24375  cbvitg  24376  itggt0  24442  dvlipcn  24591  dvfsumle  24618  dvfsumabs  24620  dvfsumlem2  24624  dvfsumlem4  24626  dvfsumrlim  24628  dvfsum2  24631  rlimcnp  25543  lgamgulmlem2  25607  lgamgulmlem6  25611  dchrisumlema  26064  dchrisumlem2  26066  dchrisumlem3  26067  chirred  30172  iundisjf  30339  fmptcof2  30402  fsumiunle  30545  esumfsup  31329  esum2d  31352  measvunilem  31471  measvunilem0  31472  nosupbnd1  33214  nosupbnd2  33216  phpreu  34891  poimirlem26  34933  poimirlem27  34934  poimirlem28  34935  itggt0cn  34979  ftc1anclem5  34986  cdleme26ee  37511  cdlemefs32sn1aw  37565  cdleme41sn3a  37584  cdleme32d  37595  cdleme32f  37597  cdlemk38  38066  cdlemk11t  38097  monotoddzz  39589  oddcomabszz  39590  evth2f  41321  evthf  41333  rfcnpre3  41339  rfcnpre4  41340  rfcnnnub  41342  ssfiunibd  41625  uzub  41754  supxrleubrnmptf  41776  infrpgernmpt  41790  monoordxr  41808  monoord2xr  41810  fsumlessf  41907  fmul01  41910  fmul01lt1lem1  41914  fmul01lt1  41916  climinff  41941  idlimc  41956  limcperiod  41958  fnlimabslt  42009  limsupref  42015  limsupbnd1f  42016  climbddf  42017  limsuppnfd  42032  climinf2  42037  limsuppnf  42041  limsupubuz  42043  climinf2mpt  42044  climinfmpt  42045  limsupmnf  42051  limsupre2  42055  limsupmnfuz  42057  limsupre3  42063  limsupre3uz  42066  limsupreuz  42067  climuz  42074  limsupgt  42108  liminfreuz  42133  liminflt  42135  xlimpnfxnegmnf  42144  xlimmnf  42171  xlimpnf  42172  dfxlim2  42178  cncfshift  42206  cncficcgt0  42220  stoweidlem3  42337  stoweidlem26  42360  stoweidlem28  42362  stoweidlem31  42365  stoweidlem51  42385  stoweidlem52  42386  stoweidlem59  42393  stirling  42423  fourierdlem20  42461  fourierdlem79  42519  etransclem48  42616  sge0ltfirp  42731  sge0lempt  42741  meaiunincf  42814  iunhoiioolem  43006  pimltmnf2  43028  pimgtpnf2  43034  pimltpnf2  43040  pimgtmnf2  43041  pimdecfgtioc  43042  issmff  43060  smfpimltxrmpt  43084  smfpreimagtf  43093  smflim  43102  smfpimgtxr  43105  smfpimgtxrmpt  43109  smfsup  43137  smfinflem  43140  smfinf  43141  nfafv2  43466  prmdvdsfmtnof1lem1  43795  dffun3f  44834  setrec2  44847