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

Theorem nfbr 3944
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 3943 . 2 (⊤ → Ⅎ𝑥 𝐴𝑅𝐵)
87mptru 1325 1 𝑥 𝐴𝑅𝐵
Colors of variables: wff set class
Syntax hints:  wtru 1317  wnf 1421  wnfc 2245   class class class wbr 3899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662  df-un 3045  df-sn 3503  df-pr 3504  df-op 3506  df-br 3900
This theorem is referenced by:  sbcbrg  3952  nfpo  4193  nfso  4194  pofun  4204  nfse  4233  nffrfor  4240  nfwe  4247  nfco  4674  nfcnv  4688  dfdmf  4702  dfrnf  4750  nfdm  4753  dffun6f  5106  dffun4f  5109  nffv  5399  funfvdm2f  5454  fvmptss2  5464  f1ompt  5539  fmptco  5554  nfiso  5675  nfofr  5956  ofrfval2  5966  tposoprab  6145  xpcomco  6688  nfsup  6847  caucvgprprlemaddq  7484  lble  8673  nfsum1  11093  nfsum  11094  fsum00  11199  mertenslem2  11273  oddpwdclemdvds  11775  oddpwdclemndvds  11776
  Copyright terms: Public domain W3C validator