ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfbr GIF version

Theorem nfbr 3881
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
StepHypRef Expression
1 nfbr.1 . . . 4 𝑥𝐴
21a1i 9 . . 3 (⊤ → 𝑥𝐴)
3 nfbr.2 . . . 4 𝑥𝑅
43a1i 9 . . 3 (⊤ → 𝑥𝑅)
5 nfbr.3 . . . 4 𝑥𝐵
65a1i 9 . . 3 (⊤ → 𝑥𝐵)
72, 4, 6nfbrd 3880 . 2 (⊤ → Ⅎ𝑥 𝐴𝑅𝐵)
87mptru 1298 1 𝑥 𝐴𝑅𝐵
Colors of variables: wff set class
Syntax hints:  wtru 1290  wnf 1394  wnfc 2215   class class class wbr 3837
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-v 2621  df-un 3001  df-sn 3447  df-pr 3448  df-op 3450  df-br 3838
This theorem is referenced by:  sbcbrg  3886  nfpo  4119  nfso  4120  pofun  4130  nfse  4159  nffrfor  4166  nfwe  4173  nfco  4589  nfcnv  4603  dfdmf  4617  dfrnf  4664  nfdm  4667  dffun6f  5015  dffun4f  5018  nffv  5299  funfvdm2f  5353  fvmptss2  5363  f1ompt  5434  fmptco  5448  nfiso  5567  nfofr  5844  ofrfval2  5853  tposoprab  6027  xpcomco  6522  nfsup  6666  caucvgprprlemaddq  7246  lble  8380  nfsum1  10709  nfsum  10710  fsum00  10819  oddpwdclemdvds  11230  oddpwdclemndvds  11231
  Copyright terms: Public domain W3C validator